theorem Th35: :: CARD_5:36

for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) = card X