theorem Th7: :: POLYALGX:7

for b1, b2 being bag of 1 holds b1 -' b2 = 1 --> ((b1 . 0) -' (b2 . 0))