let n be Ordinal; :: thesis: for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= b2,T iff not b2 < b1,T )
let T be connected TermOrder of n; :: thesis: for b1, b2 being bag of n holds
( b1 <= b2,T iff not b2 < b1,T )
let b1, b2 be bag of n; :: 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 Lm2; :: thesis: verum
end;
suppose A2: b1 <> b2 ; :: thesis: ( b1 <= b2,T iff not b2 < b1,T )
A3: ( not b2 < b1,T implies b1 <= b2,T )
proof
assume A4: not b2 < b1,T ; :: thesis: b1 <= b2,T
now :: thesis: ( ( not b2 <= b1,T & b1 <= b2,T ) or ( b1 = b2 & b1 <= b2,T ) )
per cases ( not b2 <= b1,T or b1 = b2 ) by A4;
case A5: not b2 <= b1,T ; :: thesis: b1 <= b2,T
A6: ( b1 in field T & b2 in field T ) by Lm4;
not [b2,b1] in T by A5;
then [b1,b2] in T by A1, A2, A6, RELAT_2:def 6;
hence b1 <= b2,T ; :: 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;
( b1 <= b2,T implies not b2 < b1,T ) by Lm3;
hence ( b1 <= b2,T iff not b2 < b1,T ) by A3; :: thesis: verum
end;
end;