theorem Th13: :: POLYALGX:13

for b being bag of 1 holds rng (divisors b) = { x where x is bag of 1 : x . 0 <= b . 0 }