let p be Point of (TOP-REAL 2); :: thesis: ( p `2 = 0 implies for x being real number
for r being real positive number st (+ x,r) . p = 1 holds
ex r1 being real positive number st (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,r) " {1} )
assume A1: p `2 = 0 ; :: thesis: for x being real number
for r being real positive number st (+ x,r) . p = 1 holds
ex r1 being real positive number st (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,r) " {1}
let x be real number ; :: thesis: for r being real positive number st (+ x,r) . p = 1 holds
ex r1 being real positive number st (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,r) " {1}
let r be real positive number ; :: thesis: ( (+ x,r) . p = 1 implies ex r1 being real positive number st (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,r) " {1} )
set r1 = (|.(p - |[x,r]|).| - r) / 2;
set f = + x,r;
assume A2: (+ x,r) . p = 1 ; :: thesis: ex r1 being real positive number st (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,r) " {1}
A3: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then (p `1 ) - x <> 0 by A1, A2, Def5;
then ((p `1 ) - x) ^2 > 0 by SQUARE_1:74;
then ( (((p `1 ) - x) ^2 ) + ((0 - r) ^2 ) > 0 + ((0 - r) ^2 ) & (0 - r) ^2 = (r - 0 ) ^2 ) by XREAL_1:8;
then |.|[((p `1 ) - x),((p `2 ) - r)]|.| ^2 > r ^2 by A1, Th13;
then ( |.(p - |[x,r]|).| >= 0 & |.(p - |[x,r]|).| ^2 > r ^2 ) by A3, EUCLID:66;
then |.(p - |[x,r]|).| > r by SQUARE_1:77;
then |.(p - |[x,r]|).| - r > 0 by XREAL_1:52;
then (|.(p - |[x,r]|).| - r) / 2 > 0 / 2 ;
then reconsider r1 = (|.(p - |[x,r]|).| - r) / 2 as real positive number ;
take r1 ; :: thesis: (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,r) " {1}
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in (Ball |[(p `1 ),r1]|,r1) \/ {p} or u in (+ x,r) " {1} )
assume A4: u in (Ball |[(p `1 ),r1]|,r1) \/ {p} ; :: thesis: u in (+ x,r) " {1}
then A5: ( u in Ball |[(p `1 ),r1]|,r1 or u = p ) by SETWISEO:6;
reconsider q = u as Point of (TOP-REAL 2) by A4;
Ball |[(p `1 ),r1]|,r1 c= y>=0-plane by Th24;
then reconsider z = q as Point of Niemytzki-plane by A1, A3, A5, Lm1, Th22;
A6: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
z in y>=0-plane by Lm1;
then A7: q `2 >= 0 by A6, Th22;

now

assume A8: q in Ball |[(p `1 ),r1]|,r1 ; :: thesis: ( not q in Ball |[x,r]|,r & q `2 <> 0 )
then ( |.(q - |[(p `1 ),r1]|).| < r1 & r1 is Real ) by TOPREAL9:7;
then ( |.(q - |[(p `1 ),r1]|).| + |.(|[(p `1 ),r1]| - p).| < r1 + |.(|[(p `1 ),r1]| - p).| & |.(q - |[(p `1 ),r1]|).| + |.(|[(p `1 ),r1]| - p).| >= |.(q - p).| & |.r1.| = r1 & |[(p `1 ),r1]| - p = |[((p `1 ) - (p `1 )),(r1 - 0 )]| & |.|[0 ,r1]|.| = |.r1.| ) by A1, A3, ABSVALUE:def 1, EUCLID:66, TOPREAL6:31, TOPRNS_1:35, XREAL_1:8;
then r1 + r1 > |.(q - p).| by XXREAL_0:2;
then ( |.(q - p).| + |.(|[x,r]| - q).| >= |.(|[x,r]| - p).| & (|.(p - |[x,r]|).| - r) + |.(|[x,r]| - q).| > |.(q - p).| + |.(|[x,r]| - q).| ) by TOPRNS_1:35, XREAL_1:8;
then |.(|[x,r]| - p).| < (|.(p - |[x,r]|).| - r) + |.(|[x,r]| - q).| by XXREAL_0:2;
then ( |.(p - |[x,r]|).| = |.(|[x,r]| - p).| & |.(|[x,r]| - p).| - (|.(p - |[x,r]|).| - r) < |.(|[x,r]| - q).| ) by TOPRNS_1:28, XREAL_1:21;
then |.(q - |[x,r]|).| > r by TOPRNS_1:28;
hence not q in Ball |[x,r]|,r by TOPREAL9:7; :: thesis: q `2 <> 0
( q `2 = 0 implies ( q in y=0-line & Ball |[(p `1 ),r1]|,r1 misses y=0-line ) ) by A6, Th25;
hence q `2 <> 0 by A8, XBOOLE_0:3; :: thesis: verum

end;

then (+ x,r) . z = 1 by A2, A4, A6, A7, Def5, SETWISEO:6;
then (+ x,r) . z in {1} by TARSKI:def 1;
hence u in (+ x,r) " {1} by FUNCT_2:46; :: thesis: verum