let A be denumerable set ; :: thesis: NAT ,A are_equipotent
not card A in omega ;
then A1: omega c= card A by CARD_1:14;
card A c= omega by CARD_3:def 15;
then card NAT = card A by A1, CARD_1:84, XBOOLE_0:def 10;
hence NAT ,A are_equipotent by CARD_1:21; :: thesis: verum