let X be set ; :: thesis: ( not X is finite & X c= omega implies card X = omega )
assume A1: ( not X is finite & X c= omega ) ; :: thesis: card X = omega
NAT ,X are_equipotent by A1, WAYBEL12:3;
hence card X = omega by CARD_1:21, CARD_1:84; :: thesis: verum