theorem :: CLASSES4:108

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