let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x, a being real number
for r being real positive number 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 number
for r being real positive number 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 real non negative number by A1;
let x, a be real number ; :: thesis: for r being real positive number st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds
(+ x,r) . p > a
let r be real positive number ; :: 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 real non negative number by A2;
reconsider ra = r * a as Real by XREAL_0:def 1;
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:28
.= |.|[(x - x),(ra - 0 )]|.| by EUCLID:66
.= abs ra by TOPREAL6:31
.= r * a9 by ABSVALUE:def 1 ;
then A5: ( p `1 <> x or p2 <> 0 ) by A4, EUCLID:57;
A6: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then reconsider z = p as Element of Niemytzki-plane by A1, Lm1, Th22;
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:29;
then (+ x,r) . p <> 0 by A1, Th64;
hence (+ x,r) . p > a by A7, A8, BORSUK_1:83, 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:56;
A11: |[((p `1 ) - x),p2]| `2 = p2 by EUCLID:56;
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:28
.= (|.|[((p `1 ) - x),(p2 - 0 )]|.| ^2 ) / ((2 * r) * p2) by A6, EUCLID:66
.= ((((p `1 ) - x) ^2 ) + (p2 ^2 )) / ((2 * r) * p2) by A10, A11, JGRAPH_1:46 ;
|.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2 by A2, A4, SQUARE_1:78;
then A14: |.|[((p `1 ) - x),(p2 - (r * a))]|.| ^2 > (r * a) ^2 by A6, EUCLID:66;
A15: |[((p `1 ) - x),(p2 - (r * a))]| `2 = p2 - (r * a) by EUCLID:56;
|[((p `1 ) - x),(p2 - (r * a))]| `1 = (p `1 ) - x by EUCLID:56;
then (((p `1 ) - x) ^2 ) + ((p2 - (r * a)) ^2 ) > (r * a) ^2 by A14, A15, JGRAPH_1:46;
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:34;
then A16: (((p `1 ) - x) ^2 ) + (p2 ^2 ) > ((2 * p2) * r) * a by XREAL_1:49;
A17: ( p2 = 0 implies p in y=0-line ) by A6;
Ball |[x,r]|,r misses y=0-line by Th25;
then reconsider p2 = p2 as real positive number 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:76;
hence (+ x,r) . p > a by A18, XCMPLX_1:75; :: thesis: verum

end;

end;