:: deftheorem Def5 defines + TOPGEN_5:def 5 :
for x being Real
for r being positive Real
for b₃ being Function of Niemytzki-plane,I[01] holds
( b₃ = + (x,r) iff ( b₃ . |[x,0]| = 0 & ( for a being Real
for b being non negative Real holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b₃ . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies b₃ . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) ) );