:: deftheorem Def5 defines absint INT_3:def 5 :
for b₁ being Function of INT.Ring,NAT holds
( b₁ = absint iff for a being Element of INT.Ring holds b₁ . a = absreal . a );