theorem Th12: :: POLYALGX:12

for b1, b2 being bag of 1 holds
( ( b2 in rng (divisors b1) implies b2 . 0 <= b1 . 0 ) & ( b2 . 0 <= b1 . 0 implies b2 in rng (divisors b1) ) & ( b2 in rng (divisors b1) implies b2 divides b1 ) & ( b2 divides b1 implies b2 in rng (divisors b1) ) )