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

now :: thesis: for p being object st p in n holds
not d . p <> b . p

defpred S₁[ set ] means d . $1 < b . $1;
let p be object ; :: thesis: ( p in n implies not d . p <> b . p )
assume p in n ; :: thesis: not d . p <> b . p
then reconsider p9 = p as Ordinal ;
assume A3: d . p <> b . p ; :: thesis: contradiction
d . p9 <= b . p9 by A1;
then d . p9 < b . p9 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 :: thesis: for l being Ordinal st l in k holds
d . l = b . l

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:5;
d . l <= b . l by A1;
hence d . l = b . l by A7, XXREAL_0:1; :: thesis: verum

end;

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

end;

hence d = b ; :: thesis: verum