theorem Th8: :: POLYALGX:8

for b1, b2 being bag of 1 holds
( b1 . 0 <= b2 . 0 iff b1 divides b2 )