let p be Point of (TOP-REAL 2); :: thesis:
assume A1: p `2 > 0 ; :: thesis:
let x, a be real number ; :: thesis:
let r be real positive number ; :: 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:57;
then p in the carrier of Niemytzki-plane by A1, Lm1;
then (+ x,r) . p in the carrier of I[01] by FUNCT_2:7;
then (+ x,r) . p <= 1 by BORSUK_1:83, 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 real positive number by A1;
reconsider A = Ball p,r1 as Subset of Niemytzki-plane by A4, Lm1, Th24;
take r1 ; :: thesis:
thus r1 <= p `2 ; :: thesis:
let u be set ; :: 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:57;
q in A by A7;
then A9: q `2 >= 0 by A8, Lm1, Th22;
q in A by A7;
then reconsider z = q as Element of Niemytzki-plane ;
A11: (+ x,r) . z >= 0 by BORSUK_1:83, XXREAL_1:1;
y=0-line misses Ball p,r1 by A4, Th25;
then not q in y=0-line by A7, XBOOLE_0:3;
then A12: q `2 <> 0 by A8;
A13: (+ x,r) . z <= 1 by BORSUK_1:83, XXREAL_1:1;
|[x,0 ]| `2 = 0 by EUCLID:56;
then (+ x,r) . q <> 0 by A12, A9, Th64;
then (+ x,r) . z in ].a,1.] by A11, A13, A6, XXREAL_1:2;
hence u in (+ x,r) " ].a,1.] by FUNCT_2:46; :: thesis:

end;

suppose a > 0 ; :: thesis:

then reconsider b = a as real positive number ;
set r1 = min (|.(p - |[x,(r * a)]|).| - (r * a)),(p `2 );
A14: ( 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;
A15: b <> (+ x,r) . p by A3;
not |.(p - |[x,(r * a)]|).| < r * a by A3, A5, Th67;
then |.(p - |[x,(r * a)]|).| > r * a by A15, A1, A5, Th66, XXREAL_0:1;
then reconsider r1 = min (|.(p - |[x,(r * a)]|).| - (r * a)),(p `2 ) as real positive number by A14, A1, XREAL_1:52;
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, Th24;
let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A16: u in Ball p,r1 ; :: thesis:
then reconsider q = u as Point of (TOP-REAL 2) ;
u in A by A16;
then reconsider z = q as Point of Niemytzki-plane ;
A17: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
q in A by A16;
then A18: q `2 >= 0 by A17, Lm1, Th22;

A19: now

|.(p - |[x,(r * a)]|).| - (r * a) >= r1 by XXREAL_0:17;
then A20: (r * a) + r1 <= (|.(p - |[x,(r * a)]|).| - (r * a)) + (r * a) by XREAL_1:8;
assume not (+ x,r) . z > a ; :: thesis:
then |.(q - |[x,(r * a)]|).| <= r * a by A2, A5, A18, Th68;
then A21: |.(|[x,(r * a)]| - q).| <= r * a by TOPRNS_1:28;
A22: |.(|[x,(r * a)]| - q).| + |.(q - p).| >= |.(|[x,(r * a)]| - p).| by TOPRNS_1:35;
|.(q - p).| < r1 by A16, TOPREAL9:7;
then |.(|[x,(r * a)]| - q).| + |.(q - p).| < (r * a) + r1 by A21, XREAL_1:10;
then |.(|[x,(r * a)]| - p).| < (r * a) + r1 by A22, XXREAL_0:2;
hence contradiction by A20, TOPRNS_1:28; :: thesis:

end;

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

end;

end;