let X be set ; :: thesis:
thus ( not X is finite implies ex Y being set st
( Y c= X & card Y = omega ) ) :: thesis:

assume not X is finite ; :: thesis:
then not card X in omega ;
then A1: omega c= card X by CARD_1:4;
card X,X are_equipotent by CARD_1:def 2;
then consider f being Function such that
A2: f is one-to-one and
A3: dom f = card X and
A4: rng f = X ;
take Y = f .: omega; :: thesis:
thus Y c= X by A4, RELAT_1:111; :: thesis:
omega ,Y are_equipotent

take f | omega ; :: according to WELLORD2:def 4 :: thesis:
thus ( f | omega is one-to-one & proj1 (f | omega) = omega & proj2 (f | omega) = Y ) by A1, A2, A3, FUNCT_1:52, RELAT_1:62, RELAT_1:115; :: thesis:

end;

hence card Y = omega by CARD_1:def 2; :: thesis:

end;

given Y being set such that A5: Y c= X and
A6: card Y = omega ; :: thesis:
thus not X is finite by A5, A6; :: thesis: