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 a2 < a1 )
let a1, a2 be Element of A; :: thesis: ( not A is strongly_connected or a1 = a2 or a1 < a2 or a2 < a1 )
assume A is strongly_connected ; :: thesis: ( a1 = a2 or a1 < a2 or a2 < a1 )
then A1: ( a1 <= a2 or a2 <= a1 ) by Th25;
assume A2: not a1 = a2 ; :: thesis: ( a1 < a2 or a2 < a1 )
assume not a1 < a2 ; :: thesis: a2 < a1
then not a1 <= a2 by A2, ORDERS_2:def 6;
hence a2 < a1 by A1, A2, ORDERS_2:def 6; :: thesis: verum