let p be Point of (TOP-REAL 2); :: thesis:
assume A1: p `2 > 0 ; :: thesis:
let x, a be Real; :: thesis:
let r be positive Real; :: thesis:
set f = + (x,r);
assume that
A2: 0 <= a and
A3: a < (+ (x,r)) . p ; :: thesis:
A4: p = |[(p `1),(p `2)]| by EUCLID:53;
then p in the carrier of Niemytzki-plane by A1, Lm1;
then (+ (x,r)) . p in the carrier of I[01] by FUNCT_2:5;
then (+ (x,r)) . p <= 1 by BORSUK_1:40, XXREAL_1:1;
then A5: a < 1 by A3, XXREAL_0:2;

per cases by A2;

suppose A6: a = 0 ; :: thesis:

reconsider r1 = p `2 as positive Real by A1;
reconsider A = Ball (p,r1) as Subset of Niemytzki-plane by A4, Lm1, Th20;
take r1 ; :: thesis:
thus r1 <= p `2 ; :: thesis:
let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: u in Ball (p,r1) ; :: thesis:
then reconsider q = u as Point of (TOP-REAL 2) ;
A8: q = |[(q `1),(q `2)]| by EUCLID:53;
q in A by A7;
then A9: q `2 >= 0 by A8, Lm1, Th18;
q in A by A7;
then reconsider z = q as Element of Niemytzki-plane ;
A10: (+ (x,r)) . z >= 0 by BORSUK_1:40, XXREAL_1:1;
y=0-line misses Ball (p,r1) by A4, Th21;
then not q in y=0-line by A7, XBOOLE_0:3;
then A11: q `2 <> 0 by A8;
A12: (+ (x,r)) . z <= 1 by BORSUK_1:40, XXREAL_1:1;
|[x,0]| `2 = 0 by EUCLID:52;
then (+ (x,r)) . q <> 0 by A11, A9, Th60;
then (+ (x,r)) . z in ].a,1.] by A10, A12, A6, XXREAL_1:2;
hence u in (+ (x,r)) " ].a,1.] by FUNCT_2:38; :: thesis:

end;

suppose a > 0 ; :: thesis:

then reconsider b = a as positive Real ;
set r1 = min ((|.(p - |[x,(r * a)]|).| - (r * a)),(p `2));
A13: ( min ((|.(p - |[x,(r * a)]|).| - (r * a)),(p `2)) = |.(p - |[x,(r * a)]|).| - (r * a) or min ((|.(p - |[x,(r * a)]|).| - (r * a)),(p `2)) = p `2 ) by XXREAL_0:def 9;
A14: b <> (+ (x,r)) . p by A3;
not |.(p - |[x,(r * a)]|).| < r * a by A3, A5, Th63;
then |.(p - |[x,(r * a)]|).| > r * a by A14, A1, A5, Th62, XXREAL_0:1;
then reconsider r1 = min ((|.(p - |[x,(r * a)]|).| - (r * a)),(p `2)) as positive Real by A13, A1, XREAL_1:50;
take r1 ; :: thesis:
thus r1 <= p `2 by XXREAL_0:17; :: thesis:
then reconsider A = Ball (p,r1) as Subset of Niemytzki-plane by A4, Lm1, Th20;
let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: u in Ball (p,r1) ; :: thesis:
then reconsider q = u as Point of (TOP-REAL 2) ;
u in A by A15;
then reconsider z = q as Point of Niemytzki-plane ;
A16: q = |[(q `1),(q `2)]| by EUCLID:53;
q in A by A15;
then A17: q `2 >= 0 by A16, Lm1, Th18;

A18: now :: thesis:

|.(p - |[x,(r * a)]|).| - (r * a) >= r1 by XXREAL_0:17;
then A19: (r * a) + r1 <= (|.(p - |[x,(r * a)]|).| - (r * a)) + (r * a) by XREAL_1:6;
assume not (+ (x,r)) . z > a ; :: thesis:
then |.(q - |[x,(r * a)]|).| <= r * a by A2, A5, A17, Th64;
then A20: |.(|[x,(r * a)]| - q).| <= r * a by TOPRNS_1:27;
A21: |.(|[x,(r * a)]| - q).| + |.(q - p).| >= |.(|[x,(r * a)]| - p).| by TOPRNS_1:34;
|.(q - p).| < r1 by A15, TOPREAL9:7;
then |.(|[x,(r * a)]| - q).| + |.(q - p).| < (r * a) + r1 by A20, XREAL_1:8;
then |.(|[x,(r * a)]| - p).| < (r * a) + r1 by A21, XXREAL_0:2;
hence contradiction by A19, TOPRNS_1:27; :: thesis:

end;

(+ (x,r)) . z <= 1 by BORSUK_1:40, XXREAL_1:1;
then (+ (x,r)) . z in ].a,1.] by A18, XXREAL_1:2;
hence u in (+ (x,r)) " ].a,1.] by FUNCT_2:38; :: thesis:

end;

end;