theorem Th109: :: CLASSES4:109

for n being Nat holds not ComplUniverse . n is empty