:: deftheorem Def3 defines Intervals EUCLID_9:def 3 :
for f being real-valued Function
for r being Real
for b₃ being Function holds
( b₃ = Intervals (f,r) iff ( dom b₃ = dom f & ( for x being object st x in dom f holds
b₃ . x = ].((f . x) - r),((f . x) + r).[ ) ) );