theorem :: CLASSES4:59

for UN being non trivial Universe
for n being Nat holds REAL n in UN