let n be Ordinal; :: thesis:
let b1, b2 be bag of n; :: thesis:

A1: now :: thesis:

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

now :: thesis:

per cases ;

case b1 = b2 ; :: thesis:

hence b2 <=' b1 ; :: thesis:

end;

case b1 <> b2 ; :: thesis:

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

end;

end;

end;

hence b2 <=' b1 ; :: thesis:

end;

now :: thesis:

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

now :: thesis:

per cases ;

case b2 <> b1 ; :: thesis:

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

end;

case b1 = b2 ; :: thesis:

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:

end;

end;

end;

hence not b1 < b2 ; :: thesis:

end;

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