theorem Th16: :: CLASSES4:16

for UN being Universe
for n being Nat holds n in UN