let p be Point of (TOP-REAL 2); :: thesis:
assume A1: p `2 >= 0 ; :: thesis:
let x, a, b be Real; :: thesis:
let r be positive Real; :: thesis:
A2: p = |[(p `1),(p `2)]| by EUCLID:53;
A3: Ball (|[x,r]|,r) misses y=0-line by Th21;
A4: |[((p `1) - x),(p `2)]| `1 = (p `1) - x by EUCLID:52;
assume that
A5: 0 <= a and
A6: b <= 1 and
A7: (+ (x,r)) . p in ].a,b.[ ; :: thesis:
A8: (+ (x,r)) . p > a by A7, XXREAL_1:4;
A9: (+ (x,r)) . p < b by A7, XXREAL_1:4;
then A10: ( p in Ball (|[x,r]|,r) or ( p `1 = x & p `2 = 0 & p <> |[x,0]| ) ) by A8, A1, A2, A5, A6, Def5;
then A11: (+ (x,r)) . p = (|.(|[x,0]| - p).| ^2) / ((2 * r) * (p `2)) by A1, A2, Def5;
( p `2 = 0 implies p in y=0-line ) by A2;
then reconsider p2 = p `2 , b9 = b as positive Real by A3, A1, A5, A8, A7, A10, EUCLID:53, XBOOLE_0:3, XXREAL_1:4;
A12: |[((p `1) - x),p2]| `2 = p2 by EUCLID:52;
A13: (2 * r) * p2 > 0 ;
then |.(|[x,0]| - p).| ^2 > ((2 * r) * (p `2)) * a by A11, A8, XREAL_1:79;
then |.(p - |[x,0]|).| ^2 > ((2 * r) * (p `2)) * a by TOPRNS_1:27;
then |.|[((p `1) - x),((p `2) - 0)]|.| ^2 > ((2 * r) * (p `2)) * a by A2, EUCLID:62;
then (((p `1) - x) ^2) + (p2 ^2) > ((2 * r) * p2) * a by A4, A12, JGRAPH_1:29;
then ((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * a) > 0 by XREAL_1:50;
then (((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * a)) + ((r * a) ^2) > (r * a) ^2 by XREAL_1:29;
then A14: (((p `1) - x) ^2) + ((p2 - (r * a)) ^2) > (r * a) ^2 ;
|.(|[x,0]| - p).| ^2 < ((2 * r) * (p `2)) * b by A13, A11, A9, XREAL_1:77;
then |.(p - |[x,0]|).| ^2 < ((2 * r) * (p `2)) * b by TOPRNS_1:27;
then |.|[((p `1) - x),((p `2) - 0)]|.| ^2 < ((2 * r) * (p `2)) * b by A2, EUCLID:62;
then (((p `1) - x) ^2) + (p2 ^2) < ((2 * r) * p2) * b by A4, A12, JGRAPH_1:29;
then ((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * b) < 0 by XREAL_1:49;
then (((((p `1) - x) ^2) + (p2 ^2)) - (((2 * r) * p2) * b)) + ((r * b) ^2) < (r * b) ^2 by XREAL_1:30;
then A15: (((p `1) - x) ^2) + ((p2 - (r * b)) ^2) < (r * b) ^2 ;
A16: |[((p `1) - x),(p2 - (r * b))]| `2 = p2 - (r * b) by EUCLID:52;
A17: |[((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),(p2 - (r * a))]|.| ^2 > (r * a) ^2 by A14, A17, JGRAPH_1:29;
then |.(p - |[x,(r * a)]|).| ^2 > (r * a) ^2 by A2, EUCLID:62;
then A18: |.(p - |[x,(r * a)]|).| > r * a by SQUARE_1:48;
A19: ((r * b) - |.(p - |[x,(r * b)]|).|) + |.(p - |[x,(r * b)]|).| = r * b ;
set r1 = min (((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a)));
A20: |.(p - |[x,(r * b)]|).| = |.(|[x,(r * b)]| - p).| by TOPRNS_1:27;
|[((p `1) - x),(p2 - (r * b))]| `1 = (p `1) - x by EUCLID:52;
then |.|[((p `1) - x),(p2 - (r * b))]|.| ^2 < (r * b) ^2 by A15, A16, JGRAPH_1:29;
then A21: |.(p - |[x,(r * b)]|).| ^2 < (r * b) ^2 by A2, EUCLID:62;
r * b9 >= 0 ;
then |.(p - |[x,(r * b)]|).| < r * b by A21, SQUARE_1:48;
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 A18, XREAL_1:50, XXREAL_0:15;
then reconsider r1 = min (((r * b) - |.(p - |[x,(r * b)]|).|),(|.(p - |[x,(r * a)]|).| - (r * a))) as positive Real ;
take r1 ; :: thesis:
r1 <= (r * b) - |.(p - |[x,(r * b)]|).| by XXREAL_0:17;
then A22: |.(|[x,(r * b)]| - p).| + r1 <= r * b by A20, A19, XREAL_1:6;
|.(p - |[(p `1),0]|).| = |.|[((p `1) - (p `1)),(p2 - 0)]|.| by A2, EUCLID:62
.= |.p2.| by TOPREAL6:23
.= p2 by ABSVALUE:def 1 ;
then A23: |.(|[x,(r * b)]| - |[(p `1),0]|).| <= |.(|[x,(r * b)]| - p).| + p2 by TOPRNS_1:34;

hereby :: thesis:

assume r1 > p `2 ; :: thesis:
then |.(|[x,(r * b)]| - p).| + p2 < |.(|[x,(r * b)]| - p).| + r1 by XREAL_1:8;
then |.(|[x,(r * b)]| - |[(p `1),0]|).| < |.(|[x,(r * b)]| - p).| + r1 by A23, XXREAL_0:2;
then |.(|[x,(r * b)]| - |[(p `1),0]|).| < r * b by A22, XXREAL_0:2;
then |.(|[(p `1),0]| - |[x,(r * b)]|).| < r * b by TOPRNS_1:27;
then A24: |[(p `1),0]| in Ball (|[x,(r * b)]|,(r * b)) by TOPREAL9:7;
|[(p `1),0]| in y=0-line ;
then Ball (|[x,(r * b)]|,(r * b9)) meets y=0-line by A24, XBOOLE_0:3;
hence contradiction by Th21; :: thesis:

end;

then A25: Ball (p,r1) c= y>=0-plane by A2, Th20;
let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: u in Ball (p,r1) ; :: thesis:
then reconsider q = u as Point of (TOP-REAL 2) ;
A27: |.(q - p).| < r1 by A26, TOPREAL9:7;
then |.(q - p).| + |.(p - |[x,(r * b)]|).| < r1 + |.(p - |[x,(r * b)]|).| by XREAL_1:8;
then A28: |.(q - p).| + |.(p - |[x,(r * b)]|).| < r * b by A20, A22, XXREAL_0:2;
|.(q - |[x,(r * b)]|).| <= |.(q - p).| + |.(p - |[x,(r * b)]|).| by TOPRNS_1:34;
then |.(q - |[x,(r * b)]|).| < r * b by A28, XXREAL_0:2;
then A29: (+ (x,r)) . q < b by A6, Th63;
A30: |.(p - |[x,(r * a)]|).| <= |.(p - q).| + |.(q - |[x,(r * a)]|).| by TOPRNS_1:34;
a < b by A8, A9, XXREAL_0:2;
then A31: a < 1 by A6, XXREAL_0:2;
|.(p - |[x,(r * a)]|).| - (r * a) >= r1 by XXREAL_0:17;
then |.(p - |[x,(r * a)]|).| - (r * a) > |.(q - p).| by A27, XXREAL_0:2;
then A32: |.(p - |[x,(r * a)]|).| - |.(q - p).| > r * a by XREAL_1:12;
|.(p - q).| = |.(q - p).| by TOPRNS_1:27;
then |.(q - |[x,(r * a)]|).| >= |.(p - |[x,(r * a)]|).| - |.(q - p).| by A30, XREAL_1:20;
then A33: |.(q - |[x,(r * a)]|).| > r * a by A32, XXREAL_0:2;
q = |[(q `1),(q `2)]| by EUCLID:53;
then q `2 >= 0 by A25, A26, Th18;
then (+ (x,r)) . q > a by A33, A5, A31, Th64;
then (+ (x,r)) . q in ].a,b.[ by A29, XXREAL_1:4;
hence u in (+ (x,r)) " ].a,b.[ by A25, A26, Lm1, FUNCT_2:38; :: thesis: