let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x, a being Real
for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a )
assume A1: p `2 >= 0 ; :: thesis: for x, a being Real
for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a
set p1 = p `1 ;
set p2 = p `2 ;
reconsider p2 = p `2 as non negative Real by A1;
let x, a be Real; :: thesis: for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ (x,r)) . p > a
let r be positive Real; :: thesis: ( 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a implies (+ (x,r)) . p > a )
assume that
A2: 0 <= a and
A3: a < 1 ; :: thesis: ( not |.(p - |[x,(r * a)]|).| > r * a or (+ (x,r)) . p > a )
reconsider a9 = a as non negative Real by A2;
reconsider ra = r * a as Real ;
assume A4: |.(p - |[x,(r * a)]|).| > r * a ; :: thesis: (+ (x,r)) . p > a
|.(|[x,0]| - |[x,(r * a)]|).| = |.(|[x,(r * a)]| - |[x,0]|).| by TOPRNS_1:27
.= |.|[(x - x),(ra - 0)]|.| by EUCLID:62
.= |.ra.| by TOPREAL6:23
.= r * a9 by ABSVALUE:def 1 ;
then A5: ( p `1 <> x or p2 <> 0 ) by A4, EUCLID:53;
A6: p = |[(p `1),(p `2)]| by EUCLID:53;
then reconsider z = p as Element of Niemytzki-plane by A1, Lm1, Th18;
A7: (+ (x,r)) . z in the carrier of I[01] ;

per cases ( a = 0 or (+ (x,r)) . p = 1 or ( a > 0 & (+ (x,r)) . z <> 1 ) ) by A2;

suppose A8: a = 0 ; :: thesis: (+ (x,r)) . p > a

then p <> |[x,(r * 0)]| by A4, TOPRNS_1:28;
then (+ (x,r)) . p <> 0 by A1, Th60;
hence (+ (x,r)) . p > a by A7, A8, BORSUK_1:40, XXREAL_1:1; :: thesis: verum

end;

suppose (+ (x,r)) . p = 1 ; :: thesis: (+ (x,r)) . p > a

hence (+ (x,r)) . p > a by A3; :: thesis: verum

end;

suppose A9: ( a > 0 & (+ (x,r)) . z <> 1 ) ; :: thesis: (+ (x,r)) . p > a

A10: |[((p `1) - x),(p2 - 0)]| `1 = (p `1) - x by EUCLID:52;
A11: |[((p `1) - x),p2]| `2 = p2 by EUCLID:52;
not p2 is negative ;
then A12: p in Ball (|[x,r]|,r) by A6, A5, A9, Def5;
then A13: (+ (x,r)) . p = (|.(|[x,0]| - p).| ^2) / ((2 * r) * p2) by A6, Def5
.= (|.(p - |[x,0]|).| ^2) / ((2 * r) * p2) by TOPRNS_1:27
.= (|.|[((p `1) - x),(p2 - 0)]|.| ^2) / ((2 * r) * p2) by A6, EUCLID:62
.= ((((p `1) - x) ^2) + (p2 ^2)) / ((2 * r) * p2) by A10, A11, JGRAPH_1:29 ;
|.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2 by A2, A4, SQUARE_1:16;
then A14: |.|[((p `1) - x),(p2 - (r * a))]|.| ^2 > (r * a) ^2 by A6, EUCLID:62;
A15: |[((p `1) - x),(p2 - (r * a))]| `2 = p2 - (r * a) by EUCLID:52;
|[((p `1) - x),(p2 - (r * a))]| `1 = (p `1) - x by EUCLID:52;
then (((p `1) - x) ^2) + ((p2 - (r * a)) ^2) > (r * a) ^2 by A14, A15, JGRAPH_1:29;
then (((((p `1) - x) ^2) + (p2 ^2)) - ((2 * p2) * (r * a))) + ((r * a) ^2) > (r * a) ^2 ;
then ((((p `1) - x) ^2) + (p2 ^2)) - (((2 * p2) * r) * a) > 0 by XREAL_1:32;
then A16: (((p `1) - x) ^2) + (p2 ^2) > ((2 * p2) * r) * a by XREAL_1:47;
A17: ( p2 = 0 implies p in y=0-line ) by A6;
Ball (|[x,r]|,r) misses y=0-line by Th21;
then reconsider p2 = p2 as positive Real by A12, A17, XBOOLE_0:3;
A18: a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1 by XCMPLX_1:60;
(+ (x,r)) . p > (((2 * p2) * r) * a) / ((2 * r) * p2) by A13, A16, XREAL_1:74;
hence (+ (x,r)) . p > a by A18, XCMPLX_1:74; :: thesis: verum

end;

end;