let p be Point of (TOP-REAL 2); :: thesis:
assume A1: p `2 = 0 ; :: thesis:
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then reconsider p' = p as Point of Niemytzki-plane by A1, Lm1, Th22;
let x be real number ; :: thesis:
let a be real non negative number ; :: thesis:
let y, r be real positive number ; :: thesis:
set f = + x,y,r;
assume A3: (+ x,y,r) . p > a ; :: thesis:
p in y>=0-plane by A1, A2;
then (+ x,y,r) . p in [.0 ,1.] by Lm1, BORSUK_1:83, FUNCT_2:7;
then A4: (+ x,y,r) . p <= 1 by XXREAL_1:1;
then A5: a < 1 by A3, XXREAL_0:2;
A6: |.(|[x,y]| - p).| = |.(p - |[x,y]|).| by TOPRNS_1:28;
thus |.(|[x,y]| - p).| > r * a :: thesis:

proof

per cases ) . p < 1 or (+ x,y,r) . p = 1 ) by A4, XXREAL_0:1;

suppose (+ x,y,r) . p < 1 ; :: thesis:

then p in Ball |[x,y]|,r by A1, A2, Def6;
then (+ x,y,r) . p = |.(|[x,y]| - p).| / r by A1, A2, Def6;
hence |.(|[x,y]| - p).| > r * a by A3, XREAL_1:81; :: thesis:

end;

suppose A7: (+ x,y,r) . p = 1 ; :: thesis:

now

assume p in Ball |[x,y]|,r ; :: thesis:
then ( 1 = |.(|[x,y]| - p).| / r & |.(p - |[x,y]|).| < r & r / r = 1 ) by A1, A2, A7, Def6, TOPREAL9:7, XCMPLX_1:60;
hence contradiction by A6, XREAL_1:76; :: thesis:

end;

then ( |.(p - |[x,y]|).| >= r & r * 1 > r * a ) by A5, TOPREAL9:7, XREAL_1:70;
hence |.(|[x,y]| - p).| > r * a by A6, XXREAL_0:2; :: thesis:

end;

then reconsider r' = |.(|[x,y]| - p).| - (r * a) as real positive number by XREAL_1:52;
take r1 = r' / 2; :: thesis:
thus r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 ; :: thesis:
let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A8: u in (Ball |[(p `1 ),r1]|,r1) \/ {p} ; :: thesis:
then A9: ( u in Ball |[(p `1 ),r1]|,r1 or u = p' ) by SETWISEO:6;
Ball |[(p `1 ),r1]|,r1 c= y>=0-plane by Th24;
then reconsider z = u as Point of Niemytzki-plane by A9, Def3;
reconsider q = z as Element of (TOP-REAL 2) by A8;
A10: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
then A11: q `2 >= 0 by Lm1, Th22;
then A12: ( not q in Ball |[x,y]|,r implies (+ x,y,r) . q = 1 ) by A10, Def6;

per cases by A8, SETWISEO:6;

suppose u = p' ; :: thesis:

then (+ x,y,r) . z in ].a,1.] by A3, A4, XXREAL_1:2;
hence u in (+ x,y,r) " ].a,1.] by FUNCT_2:46; :: thesis:

end;

suppose u in Ball |[(p `1 ),r1]|,r1 ; :: thesis:

then |.(q - |[(p `1 ),r1]|).| < r1 by TOPREAL9:7;
then ( |.(q - |[(p `1 ),r1]|).| + |.(|[(p `1 ),r1]| - p).| < r1 + |.(|[(p `1 ),r1]| - p).| & |.(q - p).| <= |.(q - |[(p `1 ),r1]|).| + |.(|[(p `1 ),r1]| - p).| & r1 is Real ) by TOPRNS_1:35, XREAL_1:8;
then ( |.(q - p).| < r1 + |.(|[(p `1 ),r1]| - p).| & |.(|[(p `1 ),r1]| - p).| = |.|[((p `1 ) - (p `1 )),(r1 - 0 )]|.| & |.|[0 ,r1]|.| = abs r1 & abs r1 = r1 ) by A1, A2, ABSVALUE:def 1, EUCLID:66, TOPREAL6:31, XXREAL_0:2;
then ( |.(|[x,y]| - q).| + |.(q - p).| < |.(|[x,y]| - q).| + (r1 + r1) & |.(|[x,y]| - p).| <= |.(|[x,y]| - q).| + |.(q - p).| ) by TOPRNS_1:35, XREAL_1:8;
then |.(|[x,y]| - p).| < |.(|[x,y]| - q).| + (r1 + r1) by XXREAL_0:2;
then A13: |.(|[x,y]| - p).| - (r1 + r1) < (|.(|[x,y]| - q).| + (r1 + r1)) - (r1 + r1) by XREAL_1:11;

A14: now

assume q in Ball |[x,y]|,r ; :: thesis:
then (+ x,y,r) . q = |.(|[x,y]| - q).| / r by A10, A11, Def6;
hence (+ x,y,r) . z > a by A13, XREAL_1:83; :: thesis:

end;

(+ x,y,r) . z in [.0 ,1.] by BORSUK_1:83, FUNCT_2:7;
then (+ x,y,r) . z <= 1 by XXREAL_1:1;
then (+ x,y,r) . z in ].a,1.] by A5, A12, A14, XXREAL_1:2;
hence u in (+ x,y,r) " ].a,1.] by FUNCT_2:46; :: thesis:

end;