B1: not [0,0] in NAT by ARYTM_3:38;
INT = (NAT \ {[0,0]}) \/ ([:{0},NAT:] \ {[0,0]}) by NUMBERS:def 4, XBOOLE_1:42
.= NAT \/ ([:{0},NAT:] \ {[0,0]}) by ZFMISC_1:65, B1 ;
hence for b₁ being set holds
( b₁ = INT iff b₁ = NAT \/ ([:{0},NAT:] \ {[0,0]}) ) ; :: thesis: verum