theorem Th16: :: ORDINAL1:20

for X being set
for A being Ordinal st X c= A & X <> {} holds
ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )