let p be Point of (TOP-REAL 2); :: thesis: ( p `2 = 0 implies for x being real number
for a being real non negative number
for y, r being real positive number st (+ x,y,r) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,1.] ) ) )
A1: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
assume A2: p `2 = 0 ; :: thesis: for x being real number
for a being real non negative number
for y, r being real positive number st (+ x,y,r) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,1.] ) )
then reconsider p9 = p as Point of Niemytzki-plane by A1, Lm1, Th22;
let x be real number ; :: thesis: for a being real non negative number
for y, r being real positive number st (+ x,y,r) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,1.] ) )
let a be real non negative number ; :: thesis: for y, r being real positive number st (+ x,y,r) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,1.] ) )
let y, r be real positive number ; :: thesis: ( (+ x,y,r) . p > a implies ( |.(|[x,y]| - p).| > r * a & ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,1.] ) ) )
set f = + x,y,r;
p in y>=0-plane by A2, A1;
then (+ x,y,r) . p in [.0 ,1.] by Lm1, BORSUK_1:83, FUNCT_2:7;
then A3: (+ x,y,r) . p <= 1 by XXREAL_1:1;
assume A4: (+ x,y,r) . p > a ; :: thesis: ( |.(|[x,y]| - p).| > r * a & ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,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: ex r1 being real positive number st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball |[(p `1 ),r1]|,r1) \/ {p} c= (+ x,y,r) " ].a,1.] )

proof

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

suppose (+ x,y,r) . p < 1 ; :: thesis: |.(|[x,y]| - p).| > r * a

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

end;

suppose A7: (+ x,y,r) . p = 1 ; :: thesis: |.(|[x,y]| - p).| > r * a

now

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

end;

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

end;

end;

end;

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

per cases ( u = p9 or u in Ball |[(p `1 ),r1]|,r1 ) by A13, SETWISEO:6;

suppose u = p9 ; :: thesis: u in (+ x,y,r) " ].a,1.]

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

end;

suppose u in Ball |[(p `1 ),r1]|,r1 ; :: thesis: u in (+ x,y,r) " ].a,1.]

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

A23: now

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

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, A16, A23, XXREAL_1:2;
hence u in (+ x,y,r) " ].a,1.] by FUNCT_2:46; :: thesis: verum

end;

end;