theorem :: CARD_3:84

for X being set holds
( X is finite iff card X in omega ) by Th42;