:: deftheorem Def6 defines + TOPGEN_5:def 6 :
for x, y being Real
for r being positive Real
for b₄ being Function of Niemytzki-plane,I[01] holds
( b₄ = + (x,y,r) iff for a being Real
for b being non negative Real holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies b₄ . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies b₄ . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) );