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
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then reconsider z = p as Element of Niemytzki-plane by A1, Lm1, Th22;
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 A3: ( 0 <= a & a < 1 ) ; :: thesis: ( not |.(p - |[x,(r * a)]|).| > r * a or (+ x,r) . p > a )
then reconsider a' = a as real non negative number ;
reconsider ra = r * a as Real by XREAL_0:def 1;
assume A4: |.(p - |[x,(r * a)]|).| > r * a ; :: thesis: (+ x,r) . p > a
A5: (+ x,r) . z in the carrier of I[01] by FUNCT_2:7;
|.(|[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 * a' by ABSVALUE:def 1 ;
then A6: ( p `1 <> x or p2 <> 0 ) by A4, EUCLID:57;

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

suppose A7: 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 A5, A7, 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 A8: ( a > 0 & (+ x,r) . z <> 1 ) ; :: thesis: (+ x,r) . p > a

A9: ( |[((p `1 ) - x),(p2 - 0 )]| `1 = (p `1 ) - x & |[((p `1 ) - x),p2]| `2 = p2 ) by EUCLID:56;
not p2 is negative ;
then A10: p in Ball |[x,r]|,r by A2, A6, A8, Def5;
then A11: (+ x,r) . p = (|.(|[x,0 ]| - p).| ^2 ) / ((2 * r) * p2) by A2, Def5
.= (|.(p - |[x,0 ]|).| ^2 ) / ((2 * r) * p2) by TOPRNS_1:28
.= (|.|[((p `1 ) - x),(p2 - 0 )]|.| ^2 ) / ((2 * r) * p2) by A2, EUCLID:66
.= ((((p `1 ) - x) ^2 ) + (p2 ^2 )) / ((2 * r) * p2) by A9, JGRAPH_1:46 ;
r * a >= r * 0 by A3;
then |.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2 by A4, SQUARE_1:78;
then ( |.|[((p `1 ) - x),(p2 - (r * a))]|.| ^2 > (r * a) ^2 & |[((p `1 ) - x),(p2 - (r * a))]| `1 = (p `1 ) - x & |[((p `1 ) - x),(p2 - (r * a))]| `2 = p2 - (r * a) ) by A2, EUCLID:56, EUCLID:66;
then (((p `1 ) - x) ^2 ) + ((p2 - (r * a)) ^2 ) > (r * a) ^2 by 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 A12: (((p `1 ) - x) ^2 ) + (p2 ^2 ) > ((2 * p2) * r) * a by XREAL_1:49;
( Ball |[x,r]|,r c= y>=0-plane & Ball |[x,r]|,r misses y=0-line ) by Th24, Th25;
then ( p2 >= 0 & not p in y=0-line & ( p2 = 0 implies p in y=0-line ) ) by A2, A10, XBOOLE_0:3;
then reconsider p2 = p2 as real positive number ;
( (+ x,r) . p > (((2 * p2) * r) * a) / ((2 * r) * p2) & a * (((2 * p2) * r) / ((2 * r) * p2)) = a * 1 ) by A11, A12, XCMPLX_1:60, XREAL_1:76;
hence (+ x,r) . p > a by XCMPLX_1:75; :: thesis: verum

end;

end;