for A being reflexive antisymmetric RelStr
for a1, a2 being Element of A holds
( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) ) by Th6, Th11;