let n be Ordinal; :: thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T or b2 <= b1,T )
let T be connected TermOrder of n; :: thesis: for b1, b2 being bag of n holds
( b1 <= b2,T or b2 <= b1,T )
let b1, b2 be bag of n; :: thesis: ( b1 <= b2,T or b2 <= b1,T )
A1: T is_connected_in field T by RELAT_2:def 14;

per cases ( b1 = b2 or b1 <> b2 ) ;

suppose A2: b1 = b2 ; :: thesis: ( b1 <= b2,T or b2 <= b1,T )

field T = Bags n by ORDERS_1:12;
then A3: T is_reflexive_in Bags n by RELAT_2:def 9;
b1 is Element of Bags n by PRE_POLY:def 12;
then [b1,b2] in T by A2, A3, RELAT_2:def 1;
hence ( b1 <= b2,T or b2 <= b1,T ) ; :: thesis: verum

end;

suppose A4: b1 <> b2 ; :: thesis: ( b1 <= b2,T or b2 <= b1,T )

assume not b1 <= b2,T ; :: thesis: b2 <= b1,T
then A5: not [b1,b2] in T ;
( b1 in field T & b2 in field T ) by Lm4;
then [b2,b1] in T by A1, A4, A5, RELAT_2:def 6;
hence b2 <= b1,T ; :: thesis: verum

end;

end;