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 ) )
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

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

end;

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

proof

let x be set ; :: according to RELAT_2:def 7,ORDERS_2:def 11 :: thesis: for b₁ being set holds
( not x in {a1,a2} or not b₁ in {a1,a2} or [x,b₁] in the InternalRel of A or [b₁,x] in the InternalRel of A )
let y be set ; :: 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 A4: ( 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

per cases ( ( x = a1 & y = a1 ) or ( x = a1 & y = a2 ) or ( x = a2 & y = a1 ) or ( x = a2 & y = a2 ) ) by A4, 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 A3, Def9; :: 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 A2, Def9; :: 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 A2, Def9; :: 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 A3, Def9; :: 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