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.] )
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;
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then p in y>=0-plane by 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 & (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane 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: (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 A3, 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 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, A1, A2, 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 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 A12: u in (Ball p,(|.(|[x,y]| - p).| - (r * a))) /\ y>=0-plane ; :: thesis: u in (+ x,y,r) " ].a,1.]
then reconsider z = u as Point of Niemytzki-plane by Lm1, XBOOLE_0:def 4;
reconsider q = z as Element of (TOP-REAL 2) by A12;
u in Ball p,(|.(|[x,y]| - p).| - (r * a)) by A12, XBOOLE_0:def 4;
then |.(q - p).| < r1 by TOPREAL9:7;
then A13: |.(|[x,y]| - q).| + |.(q - p).| < |.(|[x,y]| - q).| + r1 by XREAL_1:8;
A14: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
then A15: q `2 >= 0 by Lm1, Th22;
|.(|[x,y]| - p).| <= |.(|[x,y]| - q).| + |.(q - p).| by TOPRNS_1:35;
then |.(|[x,y]| - p).| < |.(|[x,y]| - q).| + r1 by A13, XXREAL_0:2;
then A16: |.(|[x,y]| - p).| - r1 < (|.(|[x,y]| - q).| + r1) - r1 by XREAL_1:11;

A17: 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 A16, XREAL_1:83; :: thesis: verum

end;

(+ x,y,r) . z in [.0 ,1.] by BORSUK_1:83, FUNCT_2:7;
then A18: (+ x,y,r) . z <= 1 by XXREAL_1:1;
( not q in Ball |[x,y]|,r implies (+ x,y,r) . q = 1 ) by A15, A14, Def6;
then (+ x,y,r) . z in ].a,1.] by A18, A5, A17, XXREAL_1:2;
hence u in (+ x,y,r) " ].a,1.] by FUNCT_2:46; :: thesis: verum