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 S1[ 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 S1[p] ;
consider k being Ordinal such that
A5: S1[k] and
A6: for m being Ordinal st S1[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