let n be Ordinal; :: thesis: for b1, b2 being bag of n holds
( not b1 < b2 iff b2 <=' b1 )
let b1, b2 be bag of n; :: thesis: ( not b1 < b2 iff b2 <=' b1 )

A1: now :: thesis: ( not b1 < b2 implies b2 <=' b1 )

assume A2: not b1 < b2 ; :: thesis: b2 <=' b1

now :: thesis: ( ( b1 = b2 & b2 <=' b1 ) or ( b1 <> b2 & b2 <=' b1 ) )

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

case b1 = b2 ; :: thesis: b2 <=' b1

hence b2 <=' b1 ; :: thesis: verum

end;

case b1 <> b2 ; :: thesis: b2 <=' b1

then not b1 <=' b2 by A2, PRE_POLY:def 10;
hence b2 <=' b1 by PRE_POLY:45; :: thesis: verum

end;

end;

end;

hence b2 <=' b1 ; :: thesis: verum

end;

now :: thesis: ( b2 <=' b1 implies not b1 < b2 )

assume A3: b2 <=' b1 ; :: thesis: not b1 < b2

now :: thesis: ( ( 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 ) ) ) ) )

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

case b2 <> b1 ; :: thesis: not b1 < b2

hence not b1 < b2 by A3, PRE_POLY:def 10; :: thesis: verum

end;

case b1 = b2 ; :: thesis: for k being Ordinal holds
( not b1 . k < b2 . k or ex l being Ordinal st
( l in k & not b1 . l = b2 . l ) )

hence for k being Ordinal holds
( not b1 . k < b2 . k or ex l being Ordinal st
( l in k & not b1 . l = b2 . l ) ) ; :: thesis: verum

end;

end;

end;

hence not b1 < b2 ; :: thesis: verum

end;

hence ( not b1 < b2 iff b2 <=' b1 ) by A1; :: thesis: verum