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