let p be Point of (TOP-REAL 2); :: thesis:
assume A1: p `2 >= 0 ; :: thesis:
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
let x, a, b be real number ; :: thesis:
let r be real positive number ; :: thesis:
set r1 = min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a));
assume A3: ( 0 <= a & b <= 1 & (+ x,r) . p in ].a,b.[ ) ; :: thesis:
then A4: ( (+ x,r) . p > a & (+ x,r) . p < b ) by XXREAL_1:4;
then A5: ( p in Ball |[x,r]|,r or ( p `1 = x & p `2 = 0 & p <> |[x,0 ]| ) ) by A1, A2, A3, Def5;
a < b by A4, XXREAL_0:2;
then A6: ( 0 < b & a < 1 ) by A3, XXREAL_0:2;
( ( p `2 = 0 implies p in y=0-line ) & Ball |[x,r]|,r misses y=0-line ) by A2, Th25;
then reconsider p2 = p `2 , b' = b as real positive number by A1, A3, A4, A5, EUCLID:57, XBOOLE_0:3;
( |.(p - |[x,r]|).| < r & (2 * r) * p2 > 0 & (+ x,r) . p = (|.(|[x,0 ]| - p).| ^2 ) / ((2 * r) * (p `2 )) ) by A1, A2, A5, Def5, TOPREAL9:7;
then ( |.(|[x,0 ]| - p).| ^2 > ((2 * r) * (p `2 )) * a & |.(|[x,0 ]| - p).| ^2 < ((2 * r) * (p `2 )) * b ) by A4, XREAL_1:79, XREAL_1:81;
then ( |.(p - |[x,0 ]|).| ^2 < ((2 * r) * (p `2 )) * b & |.(p - |[x,0 ]|).| ^2 > ((2 * r) * (p `2 )) * a ) by TOPRNS_1:28;
then ( |.|[((p `1 ) - x),((p `2 ) - 0 )]|.| ^2 < ((2 * r) * (p `2 )) * b & |[((p `1 ) - x),(p `2 )]| `1 = (p `1 ) - x & |.|[((p `1 ) - x),((p `2 ) - 0 )]|.| ^2 > ((2 * r) * (p `2 )) * a & |[((p `1 ) - x),p2]| `2 = p2 ) by A2, EUCLID:56, EUCLID:66;
then ( (((p `1 ) - x) ^2 ) + (p2 ^2 ) < ((2 * r) * p2) * b & (((p `1 ) - x) ^2 ) + (p2 ^2 ) > ((2 * r) * p2) * a ) by JGRAPH_1:46;
then ( ((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * b) < 0 & ((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * a) > 0 ) by XREAL_1:51, XREAL_1:52;
then ( (((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * b)) + ((r * b) ^2 ) < (r * b) ^2 & (((((p `1 ) - x) ^2 ) + (p2 ^2 )) - (((2 * r) * p2) * a)) + ((r * a) ^2 ) > (r * a) ^2 ) by XREAL_1:31, XREAL_1:32;
then ( (((p `1 ) - x) ^2 ) + ((p2 - (r * b)) ^2 ) < (r * b) ^2 & |[((p `1 ) - x),(p2 - (r * b))]| `1 = (p `1 ) - x & (((p `1 ) - x) ^2 ) + ((p2 - (r * a)) ^2 ) > (r * a) ^2 & |[((p `1 ) - x),(p2 - (r * b))]| `2 = p2 - (r * b) & |[((p `1 ) - x),(p2 - (r * a))]| `1 = (p `1 ) - x & |[((p `1 ) - x),(p2 - (r * a))]| `2 = p2 - (r * a) ) by EUCLID:56;
then ( |.|[((p `1 ) - x),(p2 - (r * b))]|.| ^2 < (r * b) ^2 & |.|[((p `1 ) - x),(p2 - (r * a))]|.| ^2 > (r * a) ^2 ) by JGRAPH_1:46;
then ( |.(p - |[x,(r * b)]|).| ^2 < (r * b) ^2 & r * b' >= 0 & |.(p - |[x,(r * a)]|).| >= 0 & |.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2 ) by A2, EUCLID:66;
then ( |.(p - |[x,(r * b)]|).| < r * b & |.(p - |[x,(r * a)]|).| > r * a ) by SQUARE_1:118;
then ( ( (r * b) - |.(p - |[x,(r * b)]|).| > 0 & min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a)) = (r * b) - |.(p - |[x,(r * b)]|).| ) or ( |.(p - |[x,(r * a)]|).| - (r * a) > 0 & min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a)) = |.(p - |[x,(r * a)]|).| - (r * a) ) ) by XREAL_1:52, XXREAL_0:15;
then reconsider r1 = min ((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a)) as real positive number ;
take r1 ; :: thesis:
|.(p - |[(p `1 ),0 ]|).| = |.|[((p `1 ) - (p `1 )),(p2 - 0 )]|.| by A2, EUCLID:66
.= abs p2 by TOPREAL6:31
.= p2 by ABSVALUE:def 1 ;
then A7: ( |.(|[x,(r * b)]| - |[(p `1 ),0 ]|).| <= |.(|[x,(r * b)]| - p).| + p2 & r1 <= (r * b) - |.(p - |[x,(r * b)]|).| & |.(p - |[x,(r * b)]|).| = |.(|[x,(r * b)]| - p).| & ((r * b) - |.(p - |[x,(r * b)]|).|) + |.(p - |[x,(r * b)]|).| = r * b ) by TOPRNS_1:28, TOPRNS_1:35, XXREAL_0:17;
then A8: |.(|[x,(r * b)]| - p).| + r1 <= r * b by XREAL_1:8;

hereby :: thesis:

assume r1 > p `2 ; :: thesis:
then |.(|[x,(r * b)]| - p).| + p2 < |.(|[x,(r * b)]| - p).| + r1 by XREAL_1:10;
then |.(|[x,(r * b)]| - |[(p `1 ),0 ]|).| < |.(|[x,(r * b)]| - p).| + r1 by A7, XXREAL_0:2;
then |.(|[x,(r * b)]| - |[(p `1 ),0 ]|).| < r * b by A8, XXREAL_0:2;
then |.(|[(p `1 ),0 ]| - |[x,(r * b)]|).| < r * b by TOPRNS_1:28;
then ( |[(p `1 ),0 ]| in Ball |[x,(r * b)]|,(r * b) & |[(p `1 ),0 ]| in y=0-line ) by TOPREAL9:7;
then Ball |[x,(r * b)]|,(r * b') meets y=0-line by XBOOLE_0:3;
hence contradiction by Th25; :: thesis:

end;

then A9: ( Ball p,r1 c= y>=0-plane & Ball p,r1 misses y=0-line ) by A2, Th24, Th25;
let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A10: u in Ball p,r1 ; :: thesis:
then reconsider q = u as Point of (TOP-REAL 2) ;
q = |[(q `1 ),(q `2 )]| by EUCLID:57;
then A11: q `2 >= 0 by A9, A10, Th22;
( |.(p - |[x,(r * a)]|).| - (r * a) >= r1 & |.(q - p).| < r1 ) by A10, TOPREAL9:7, XXREAL_0:17;
then ( |.(q - p).| + |.(p - |[x,(r * b)]|).| < r1 + |.(p - |[x,(r * b)]|).| & |.(p - q).| = |.(q - p).| & |.(p - |[x,(r * a)]|).| <= |.(p - q).| + |.(q - |[x,(r * a)]|).| & |.(p - |[x,(r * a)]|).| - (r * a) > |.(q - p).| ) by TOPRNS_1:28, TOPRNS_1:35, XREAL_1:10, XXREAL_0:2;
then ( |.(q - |[x,(r * b)]|).| <= |.(q - p).| + |.(p - |[x,(r * b)]|).| & |.(q - p).| + |.(p - |[x,(r * b)]|).| < r * b & |.(p - |[x,(r * a)]|).| - |.(q - p).| > r * a & |.(q - |[x,(r * a)]|).| >= |.(p - |[x,(r * a)]|).| - |.(q - p).| ) by A7, A8, TOPRNS_1:35, XREAL_1:14, XREAL_1:22, XXREAL_0:2;
then ( |.(q - |[x,(r * b)]|).| < r * b & |.(q - |[x,(r * a)]|).| > r * a ) by XXREAL_0:2;
then ( (+ x,r) . q < b & (+ x,r) . q > a ) by A3, A6, A11, Th67, Th68;
then (+ x,r) . q in ].a,b.[ by XXREAL_1:4;
hence u in (+ x,r) " ].a,b.[ by A9, A10, Lm1, FUNCT_2:46; :: thesis: