theorem Th57: :: PRE_POLY:59

for n being set
for b being bag of n holds EmptyBag n divides b ;