theorem :: CLASSES4:110

for n being Nat holds ComplUniverse . n c= UNIVERSE (n + 1)