let n be Ordinal; :: thesis: for b1, b2 being bag of st b1 <=' b2 & b2 <=' b1 holds
b1 = b2
let b1, b2 be bag of ; :: thesis: ( b1 <=' b2 & b2 <=' b1 implies b1 = b2 )
assume A1: ( b1 <=' b2 & b2 <=' b1 ) ; :: thesis: b1 = b2

now

assume b1 <> b2 ; :: thesis: contradiction
then ( b1 < b2 & b2 < b1 ) by A1, POLYNOM1:def 12;
hence contradiction ; :: thesis: verum

end;

hence b1 = b2 ; :: thesis: verum