let p be Point of (TOP-REAL 2); :: thesis: ( p `2 = 0 implies for x being Real
for r being positive Real st (+ (x,r)) . p = 1 holds
ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1} )
assume A1: p `2 = 0 ; :: thesis: for x being Real
for r being positive Real st (+ (x,r)) . p = 1 holds
ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
let x be Real; :: thesis: for r being positive Real st (+ (x,r)) . p = 1 holds
ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
let r be positive Real; :: thesis: ( (+ (x,r)) . p = 1 implies ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1} )
set r1 = (|.(p - |[x,r]|).| - r) / 2;
set f = + (x,r);
A2: p = |[(p `1),(p `2)]| by EUCLID:53;
assume A3: (+ (x,r)) . p = 1 ; :: thesis: ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
then (p `1) - x <> 0 by A2, A1, Def5;
then ((p `1) - x) ^2 > 0 by SQUARE_1:12;
then (((p `1) - x) ^2) + ((0 - r) ^2) > 0 + ((0 - r) ^2) by XREAL_1:6;
then |.|[((p `1) - x),((p `2) - r)]|.| ^2 > r ^2 by A1, Th9;
then |.(p - |[x,r]|).| ^2 > r ^2 by A2, EUCLID:62;
then |.(p - |[x,r]|).| > r by SQUARE_1:15;
then |.(p - |[x,r]|).| - r > 0 by XREAL_1:50;
then reconsider r1 = (|.(p - |[x,r]|).| - r) / 2 as positive Real ;
take r1 ; :: thesis: (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}
let u be object ; :: 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 reconsider q = u as Point of (TOP-REAL 2) ;
A5: Ball (|[(p `1),r1]|,r1) c= y>=0-plane by Th20;
( u in Ball (|[(p `1),r1]|,r1) or u = p ) by A4, ZFMISC_1:136;
then reconsider z = q as Point of Niemytzki-plane by A5, A1, A2, Lm1, Th18;
A6: q = |[(q `1),(q `2)]| by EUCLID:53;

A7: now :: thesis: ( q in Ball (|[(p `1),r1]|,r1) implies ( not q in Ball (|[x,r]|,r) & q `2 <> 0 ) )

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 by TOPREAL9:7;
then A9: |.(q - |[(p `1),r1]|).| + |.(|[(p `1),r1]| - p).| < r1 + |.(|[(p `1),r1]| - p).| by XREAL_1:6;
A10: |.r1.| = r1 by ABSVALUE:def 1;
A11: |.(q - |[(p `1),r1]|).| + |.(|[(p `1),r1]| - p).| >= |.(q - p).| by TOPRNS_1:34;
A12: |.(q - p).| + |.(|[x,r]| - q).| >= |.(|[x,r]| - p).| by TOPRNS_1:34;
A13: |.|[0,r1]|.| = |.r1.| by TOPREAL6:23;
|[(p `1),r1]| - p = |[((p `1) - (p `1)),(r1 - 0)]| by A1, A2, EUCLID:62;
then r1 + r1 > |.(q - p).| by A9, A11, A10, A13, XXREAL_0:2;
then (|.(p - |[x,r]|).| - r) + |.(|[x,r]| - q).| > |.(q - p).| + |.(|[x,r]| - q).| by XREAL_1:6;
then |.(|[x,r]| - p).| < (|.(p - |[x,r]|).| - r) + |.(|[x,r]| - q).| by A12, XXREAL_0:2;
then A14: |.(|[x,r]| - p).| - (|.(p - |[x,r]|).| - r) < |.(|[x,r]| - q).| by XREAL_1:19;
|.(p - |[x,r]|).| = |.(|[x,r]| - p).| by TOPRNS_1:27;
then |.(q - |[x,r]|).| > r by A14, TOPRNS_1:27;
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, Th21;
hence q `2 <> 0 by A8, XBOOLE_0:3; :: thesis: verum

end;

z in y>=0-plane by Lm1;
then q `2 >= 0 by A6, Th18;
then (+ (x,r)) . z = 1 by A7, A3, A4, A6, Def5, ZFMISC_1:136;
then (+ (x,r)) . z in {1} by TARSKI:def 1;
hence u in (+ (x,r)) " {1} by FUNCT_2:38; :: thesis: verum