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