theorem Th99: :: CLASSES4:99

for n being Nat holds UNIVERSE n in UNIVERSE (n + 1)