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