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 & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane c= (+ x,y,r) " ].a,1.] ) )
assume A1: 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 & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane c= (+ x,y,r) " ].a,1.] )
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
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 & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane 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 & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane 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 & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane c= (+ x,y,r) " ].a,1.] ) )
set f = + x,y,r;
assume A3: (+ x,y,r) . p > a ; :: thesis: ( |.(|[x,y]| - p).| > r * a & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane c= (+ x,y,r) " ].a,1.] )
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: (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane c= (+ x,y,r) " ].a,1.]

proof

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

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

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: verum

end;

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

now

assume p in Ball |[x,y]|,r ; :: thesis: contradiction
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: verum

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: verum

end;

end;

end;

then reconsider r1 = |.(|[x,y]| - p).| - (r * a) as real positive number by XREAL_1:52;
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane or u in (+ x,y,r) " ].a,1.] )
assume A8: u in (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane ; :: thesis: u in (+ x,y,r) " ].a,1.]
then A9: ( u in Ball p,(|.(|[x,y]| - p).| - (r * a)) & u in y>=0-plane ) by XBOOLE_0:def 4;
reconsider z = u as Point of Niemytzki-plane by A8, Lm1, XBOOLE_0:def 4;
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;
|.(q - p).| < r1 by A9, TOPREAL9:7;
then ( |.(|[x,y]| - q).| + |.(q - p).| < |.(|[x,y]| - q).| + r1 & |.(|[x,y]| - p).| <= |.(|[x,y]| - q).| + |.(q - p).| ) by TOPRNS_1:35, XREAL_1:8;
then |.(|[x,y]| - p).| < |.(|[x,y]| - q).| + r1 by XXREAL_0:2;
then A13: |.(|[x,y]| - p).| - r1 < (|.(|[x,y]| - q).| + r1) - r1 by XREAL_1:11;

A14: now

assume q in Ball |[x,y]|,r ; :: thesis: (+ x,y,r) . z > a
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: 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, A12, A14, XXREAL_1:2;
hence u in (+ x,y,r) " ].a,1.] by FUNCT_2:46; :: thesis: verum