let A be reflexive RelStr ; :: thesis: for a1, a2 being Element of A holds
( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
let a1, a2 be Element of A; :: thesis: ( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
thus ( for C being Chain of A holds
( not a1 in C or not a2 in C ) or a1 <= a2 or a2 <= a1 ) :: thesis: ( ( a1 <= a2 or a2 <= a1 ) implies ex C being Chain of A st
( a1 in C & a2 in C ) )
proof
given C being Chain of A such that A1: ( a1 in C & a2 in C ) ; :: thesis: ( a1 <= a2 or a2 <= a1 )
the InternalRel of A is_strongly_connected_in C by Def7;
then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A1;
hence ( a1 <= a2 or a2 <= a1 ) ; :: thesis: verum
end;
assume A2: ( a1 <= a2 or a2 <= a1 ) ; :: thesis: ex C being Chain of A st
( a1 in C & a2 in C )
then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) ;
then reconsider B = A as non empty reflexive RelStr ;
reconsider b1 = a1, b2 = a2 as Element of B ;
reconsider Y = {b1,b2} as Chain of A by A2, Th9;
take Y ; :: thesis: ( a1 in Y & a2 in Y )
thus ( a1 in Y & a2 in Y ) by TARSKI:def 2; :: thesis: verum