theorem Th39: :: PRE_POLY:40

for X being set holds X --> 0 is bag of X