:: deftheorem Def1 defines ext-integer FVALUAT1:def 1 :
for x being object holds
( x is ext-integer iff ( x is integer or x = +infty ) );