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

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

suppose b1 = b2 ; :: thesis: ( b1 <= b2,T iff not b2 < b1,T )

hence ( b1 <= b2,T iff not b2 < b1,T ) by Def3, Lm2; :: thesis: verum

end;

suppose A2: b1 <> b2 ; :: thesis: ( b1 <= b2,T iff not b2 < b1,T )

A3: ( b1 <= b2,T implies not b2 < b1,T )

proof

assume A4: b1 <= b2,T ; :: thesis: not b2 < b1,T
assume b2 < b1,T ; :: thesis: contradiction
then ( b2 <= b1,T & b1 <> b2 ) by Def3;
hence contradiction by A4, Lm3; :: thesis: verum

end;

( not b2 < b1,T implies b1 <= b2,T )

proof

assume A5: not b2 < b1,T ; :: thesis: b1 <= b2,T

now

per cases ( not b2 <= b1,T or b1 = b2 ) by A5, Def3;

case not b2 <= b1,T ; :: thesis: b1 <= b2,T

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

end;

case b1 = b2 ; :: thesis: b1 <= b2,T

hence b1 <= b2,T by A2; :: thesis: verum

end;

end;

end;

hence b1 <= b2,T ; :: thesis: verum

end;

hence ( b1 <= b2,T iff not b2 < b1,T ) by A3; :: thesis: verum

end;

end;