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