let n be Ordinal; :: thesis: for b1, b2 being bag of n st b1 <=' b2 & b2 <=' b1 holds
b1 = b2
let b1, b2 be bag of n; :: thesis: ( b1 <=' b2 & b2 <=' b1 implies b1 = b2 )
assume that
A1: b1 <=' b2 and
A2: b2 <=' b1 ; :: thesis: b1 = b2
now :: thesis: not b1 <> b2
assume A3: b1 <> b2 ; :: thesis: contradiction
then b1 < b2 by A1, PRE_POLY:def 10;
hence contradiction by A2, A3, PRE_POLY:def 10; :: thesis: verum
end;
hence b1 = b2 ; :: thesis: verum