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: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: ( Y c= X & card Y = omega )
thus Y c= X by A4, RELAT_1:111; :: thesis: card Y = omega
omega ,Y are_equipotent

proof

take f | omega ; :: according to WELLORD2:def 4 :: thesis: ( f | omega is one-to-one & proj1 (f | omega) = omega & proj2 (f | omega) = Y )
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: verum

end;

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

end;

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