theorem Th7: :: CARD_5:7

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