let n be Ordinal; 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; for b1, b2 being bag of n holds
( b1 <= b2,T iff not b2 < b1,T )
let b1, b2 be bag of n; ( 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
;
( b1 <= b2,T iff not b2 < b1,T )hence
(
b1 <= b2,
T iff not
b2 < b1,
T )
by Lm2;
verum end; suppose A2:
b1 <> b2
;
( b1 <= b2,T iff not b2 < b1,T )A3:
( not
b2 < b1,
T implies
b1 <= b2,
T )
proof
assume A4:
not
b2 < b1,
T
;
b1 <= b2,T
now ( ( not b2 <= b1,T & b1 <= b2,T ) or ( b1 = b2 & b1 <= b2,T ) )end;
hence
b1 <= b2,
T
;
verum
end;
(
b1 <= b2,
T implies not
b2 < b1,
T )
by Lm3;
hence
(
b1 <= b2,
T iff not
b2 < b1,
T )
by A3;
verum end; end;