theorem Th65: :: PRE_POLY:67

for n being Ordinal holds divisors (EmptyBag n) = <*(EmptyBag n)*>