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:48;
hence card X in card omega ; :: thesis: verum