let A be non empty RelStr ; :: thesis: for a1, a2 being Element of A holds
( not A is strongly_connected or a1 <~ a2 or a1 =~ a2 or a1 >~ a2 )
let a1, a2 be Element of A; :: thesis: ( not A is strongly_connected or a1 <~ a2 or a1 =~ a2 or a1 >~ a2 )
assume A1: A is strongly_connected ; :: thesis: ( a1 <~ a2 or a1 =~ a2 or a1 >~ a2 )
( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A1, RELAT_2:def 7;
then A2: ( a1 <= a2 or a1 >= a2 ) by ORDERS_2:def 5;
assume ( not a1 <~ a2 & not a1 =~ a2 & not a1 >~ a2 ) ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum