theorem Th48: :: PRE_POLY:49

for n being Ordinal
for d, b being bag of n st d divides b holds
d <=' b