theorem Th3: :: MESFUNC1:3

NAT , INT are_equipotent by Th1, Th2, CARD_2:77;