theorem Th81: :: TOPGEN_5:81

for U being Subset of Niemytzki-plane
for x, y being Real
for r being positive Real st y > 0 & U = (Ball (|[x,y]|,r)) /\ y>=0-plane holds
ex f being continuous Function of Niemytzki-plane,I[01] st
( f . |[x,y]| = 0 & ( for a, b being Real holds
( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )