:: deftheorem Def1 defines INT- MESFUNC1:def 1 :
for b₁ being Subset of REAL holds
( b₁ = INT- iff for r being Real holds
( r in b₁ iff ex k being Element of NAT st r = - k ) );