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 Def3, 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
per cases ( not b2 <= b1,T or b1 = b2 ) by A4, Def3;
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, Def2;
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;
( b1 <= b2,T implies not b2 < b1,T )
proof
assume A7: 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 A7, Lm3; :: thesis: verum
end;
hence ( b1 <= b2,T iff not b2 < b1,T ) by A3; :: thesis: verum
end;
end;