NAT c= NAT \/ [:{0},NAT:] by XBOOLE_1:7;
hence NAT c= INT by ARYTM_3:32, ZFMISC_1:34; :: thesis: verum