theorem Th45: :: PRE_POLY:46

for n being set
for d, b being bag of n st ( for k being object st k in n holds
d . k <= b . k ) holds
d divides b