:: deftheorem Def3i defines integer-valued VALUED_0:def 5 :
for f being Relation holds
( f is integer-valued iff rng f c= INT );