let n be Ordinal; for b1, b2 being bag of n holds
( not b1 < b2 iff b2 <=' b1 )
let b1, b2 be bag of n; ( not b1 < b2 iff b2 <=' b1 )
A1:
now ( not b1 < b2 implies b2 <=' b1 )assume A2:
not
b1 < b2
;
b2 <=' b1now ( ( b1 = b2 & b2 <=' b1 ) or ( b1 <> b2 & b2 <=' b1 ) )end; hence
b2 <=' b1
;
verum end;
now ( b2 <=' b1 implies not b1 < b2 )assume A3:
b2 <=' b1
;
not b1 < b2now ( ( b2 <> b1 & not b1 < b2 ) or ( b1 = b2 & ( for k being Ordinal holds
( not b1 . k < b2 . k or ex l being Ordinal st
( l in k & not b1 . l = b2 . l ) ) ) ) )end; hence
not
b1 < b2
;
verum end;
hence
( not b1 < b2 iff b2 <=' b1 )
by A1; verum