theorem Th7: :: HILBASIS:7

for n being Ordinal
for b, b1 being bag of n holds
( b1 in rng (divisors b) iff b1 divides b )