theorem :: MESFUNC1:5

NAT , RAT are_equipotent