let A be non empty RelStr ; :: thesis: for a1, a2 being Element of A holds

( not A is strongly_connected or a1 <= a2 or a2 <= a1 )

let a1, a2 be Element of A; :: thesis: ( not A is strongly_connected or a1 <= a2 or a2 <= a1 )

assume A is strongly_connected ; :: thesis: ( a1 <= a2 or a2 <= a1 )

then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by RELAT_2:def 7;

hence ( a1 <= a2 or a2 <= a1 ) by ORDERS_2:def 5; :: thesis: verum

( not A is strongly_connected or a1 <= a2 or a2 <= a1 )

let a1, a2 be Element of A; :: thesis: ( not A is strongly_connected or a1 <= a2 or a2 <= a1 )

assume A is strongly_connected ; :: thesis: ( a1 <= a2 or a2 <= a1 )

then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by RELAT_2:def 7;

hence ( a1 <= a2 or a2 <= a1 ) by ORDERS_2:def 5; :: thesis: verum