theorem :: NUMBERS:17

NAT c= INT by Lm5;