:: deftheorem Def1 defines INT INT_1:def 1 :
for b₁ being set holds
( b₁ = INT iff for x being object holds
( x in b₁ iff ex k being Nat st
( x = k or x = - k ) ) );