theorem Th20: :: ORDINAL1:24

for X being set st ( for a being object st a in X holds
a is Ordinal ) holds
ex A being Ordinal st X c= A