Serial relation (source code)

= Serial relation
{title2=$\forall x\exists y\,R(x,y)$}

A <binary relation> is serial when every domain element has at least one outgoing related element. A <serial relation> may have cycles; combining seriality with an <irreflexive relation> and a <transitive relation> instead forces a nonempty domain to be infinite, by the <infinite-model property of a serial strict partial order>.