let n be set ; :: thesis: for b being bag of holds EmptyBag n divides b
let b be bag of ; :: thesis: EmptyBag n divides b
let k be set ; :: according to POLYNOM1:def 13 :: thesis: (EmptyBag n) . k <= b . k
thus (EmptyBag n) . k <= b . k by Th56; :: thesis: verum