theorem Th5: :: POLYALGX:5

for b being bag of 1 holds b = 1 --> (b . 0)