:: deftheorem Def2 defines integer INT_1:def 2 :
for i being Number holds
( i is integer iff i in INT );