{} X,X = {} ;
hence ex b₁ being Relation of X st
( b₁ is irreflexive & b₁ is asymmetric & b₁ is transitive ) ; :: thesis: verum