let I be set ; :: thesis: for m, n being bag of I holds m -' n divides m
let m, n be bag of I; :: thesis: m -' n divides m
let a be object ; :: according to PRE_POLY:def 11 :: thesis: (m -' n) . a <= m . a
(m . a) -' (n . a) <= m . a by NAT_D:35;
hence (m -' n) . a <= m . a by PRE_POLY:def 6; :: thesis: verum