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

now

let k be set ; :: thesis: ( k in n implies ((b2 -' b1) + b1) . k = b2 . k )
assume k in n ; :: thesis: ((b2 -' b1) + b1) . k = b2 . k
then reconsider k9 = k as Ordinal ;
A2: b1 . k9 <= b2 . k9 by A1, Def13;
thus ((b2 -' b1) + b1) . k = ((b2 -' b1) . k) + (b1 . k) by Def5
.= ((b2 . k) -' (b1 . k)) + (b1 . k) by Def6
.= ((b2 . k) + (b1 . k)) -' (b1 . k) by A2, NAT_D:38
.= b2 . k by NAT_D:34 ; :: thesis: verum

end;

hence (b2 -' b1) + b1 = b2 by PBOOLE:3; :: thesis: verum