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;