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

proof

assume not X is finite ; :: thesis: ex Y being set st
( Y c= X & card Y = omega )
then not card X in omega ;
then A1: omega c= card X by CARD_1:14;
card X,X are_equipotent by CARD_1:def 5;
then consider f being Function such that
A2: ( f is one-to-one & dom f = card X & rng f = X ) by WELLORD2:def 4;
take Y = f .: omega ; :: thesis: ( Y c= X & card Y = omega )
thus Y c= X by A2, RELAT_1:144; :: thesis: card Y = omega
omega ,Y are_equipotent

proof

take f | omega ; :: according to WELLORD2:def 4 :: thesis: ( f | omega is one-to-one & dom (f | omega ) = omega & rng (f | omega ) = Y )
thus ( f | omega is one-to-one & dom (f | omega ) = omega & rng (f | omega ) = Y ) by A1, A2, FUNCT_1:84, RELAT_1:91, RELAT_1:148; :: thesis: verum

end;

hence card Y = omega by CARD_1:def 5; :: thesis: verum

end;

given Y being set such that A3: ( Y c= X & card Y = omega ) ; :: thesis: not X is finite
thus not X is finite by A3; :: thesis: verum