theorem Th9: :: ORDINAL1:13

for a being object
for A being Ordinal st a in A holds
a is Ordinal