theorem :: CARD_1:61

for A being Ordinal holds
( A is finite iff A in omega ) by Lm5;