let A be non empty reflexive RelStr ; :: thesis: for a1, a2 being Element of A holds
( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
let a1, a2 be Element of A; :: thesis: ( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
A1: a2 <= a2 ;
thus ( not {a1,a2} is Chain of A or a1 <= a2 or a2 <= a1 ) :: thesis: ( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Chain of A )

proof

assume {a1,a2} is Chain of A ; :: thesis: ( a1 <= a2 or a2 <= a1 )
then A2: the InternalRel of A is_strongly_connected_in {a1,a2} by Def7;
( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def 2;
then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A2;
hence ( a1 <= a2 or a2 <= a1 ) ; :: thesis: verum

end;

assume A3: ( a1 <= a2 or a2 <= a1 ) ; :: thesis: {a1,a2} is Chain of A
A4: a1 <= a1 ;
{a1,a2} is strongly_connected

proof

let x, y be object ; :: according to RELAT_2:def 7,ORDERS_2:def 7 :: thesis: ( not x in {a1,a2} or not y in {a1,a2} or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A5: ( x in {a1,a2} & y in {a1,a2} ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

now :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

per cases ( ( x = a1 & y = a1 ) or ( x = a1 & y = a2 ) or ( x = a2 & y = a1 ) or ( x = a2 & y = a2 ) ) by A5, TARSKI:def 2;

suppose ( x = a1 & y = a1 ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A4; :: thesis: verum

end;

suppose ( x = a1 & y = a2 ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3; :: thesis: verum

end;

suppose ( x = a2 & y = a1 ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3; :: thesis: verum

end;

suppose ( x = a2 & y = a2 ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A1; :: thesis: verum

end;

end;

end;

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum

end;

hence {a1,a2} is Chain of A ; :: thesis: verum