let X be set ; :: thesis: ( X is finite implies card X in card omega )
assume X is finite ; :: thesis: card X in card omega
then ex n being Nat st card X = card n by CARD_1:86;
hence card X in card omega by CARD_1:84; :: thesis: verum