let A be reflexive antisymmetric RelStr ; :: thesis: 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 ) )
let a1, a2 be Element of A; :: thesis: ( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
thus ( ex C being Chain of A st
( a1 in C & a2 in C ) implies ( a1 < a2 iff not a2 <= a1 ) ) :: thesis: not ( ( a1 < a2 implies not a2 <= a1 ) & ( not a2 <= a1 implies a1 < a2 ) & ( for C being Chain of A holds
( not a1 in C or not a2 in C ) ) )

proof

given C being Chain of A such that A1: ( a1 in C & a2 in C ) ; :: thesis: ( a1 < a2 iff not a2 <= a1 )
thus ( a1 < a2 implies not a2 <= a1 ) by Th30; :: thesis: ( not a2 <= a1 implies a1 < a2 )
assume that
A2: not a2 <= a1 and
A3: not a1 < a2 ; :: thesis: contradiction
( not a1 <= a2 or a1 = a2 ) by A3, Def10;
hence contradiction by A1, A2, Th38; :: thesis: verum

end;

assume ( a1 < a2 iff not a2 <= a1 ) ; :: thesis: ex C being Chain of A st
( a1 in C & a2 in C )
then ( a1 <= a2 or a2 <= a1 ) by Def10;
hence ex C being Chain of A st
( a1 in C & a2 in C ) by Th38; :: thesis: verum