let A be denumerable set ; :: thesis: NAT ,A are_equipotent
not card A in omega ;
then A1: omega c= card A by CARD_1:4;
card A c= omega by CARD_3:def 14;
then card NAT = card A by A1;
hence NAT ,A are_equipotent by CARD_1:5; :: thesis: verum