theorem Th57: :: CLASSES4:57

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