theorem Th51: :: CLASSES2:51

for U being Universe holds
( On U <> {} & On U is limit_ordinal )