let n be Ordinal; :: thesis: for d, b being bag of st d divides b holds
d <=' b
let d, b be bag of ; :: thesis: ( d divides b implies d <=' b )
assume that
A1: d divides b and
A2: not d < b ; :: according to POLYNOM1:def 12 :: thesis: d = b

now

let p be set ; :: thesis: ( p in n implies not d . p <> b . p )
assume p in n ; :: thesis: not d . p <> b . p
then reconsider p' = p as Ordinal ;
A3: d . p' <= b . p' by A1, Def13;
defpred S₁[ set ] means d . $1 < b . $1;
assume d . p <> b . p ; :: thesis: contradiction
then d . p' < b . p' by A3, XXREAL_0:1;
then A4: ex p being Ordinal st S₁[p] ;
consider k being Ordinal such that
A5: S₁[k] and
A6: for m being Ordinal st S₁[m] holds
k c= m from ORDINAL1:sch 1(A4);

now

let l be Ordinal; :: thesis: ( l in k implies d . l = b . l )
assume l in k ; :: thesis: d . l = b . l
then A7: b . l <= d . l by A6, ORDINAL1:7;
d . l <= b . l by A1, Def13;
hence d . l = b . l by A7, XXREAL_0:1; :: thesis: verum

end;

hence contradiction by A2, A5, Def11; :: thesis: verum

end;

hence d = b by PBOOLE:3; :: thesis: verum