let r, r1, r2, s1, s2 be Real; :: thesis: for u being Point of (Euclid 2) st |[r1,r2]| in Ball (u,r) & |[s1,s2]| in Ball (u,r) & not |[r1,s2]| in Ball (u,r) holds
|[s1,r2]| in Ball (u,r)
let u be Point of (Euclid 2); :: thesis: ( |[r1,r2]| in Ball (u,r) & |[s1,s2]| in Ball (u,r) & not |[r1,s2]| in Ball (u,r) implies |[s1,r2]| in Ball (u,r) )
assume that
A1: |[r1,r2]| in Ball (u,r) and
A2: |[s1,s2]| in Ball (u,r) ; :: thesis: ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) )
A3: r > 0 by A1, TBSP_1:12;

per cases ( |[r1,s2]| in Ball (u,r) or not |[r1,s2]| in Ball (u,r) ) ;

suppose |[r1,s2]| in Ball (u,r) ; :: thesis: ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) )

hence ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) ) ; :: thesis: verum

end;

suppose A4: not |[r1,s2]| in Ball (u,r) ; :: thesis: ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) )

reconsider p = u as Point of (TOP-REAL 2) by EUCLID:22;
set p1 = |[r1,s2]|;
set p2 = |[s1,r2]|;
set p3 = |[s1,s2]|;
set p4 = |[r1,r2]|;
reconsider u1 = |[r1,s2]|, u2 = |[s1,r2]|, u3 = |[s1,s2]|, u4 = |[r1,r2]| as Point of (Euclid 2) by EUCLID:22;
set a = (((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2);
set b = (((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2);
set c = (((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2);
set d = (((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2);
( (Pitag_dist 2) . (u,u1) = dist (u,u1) & r <= dist (u,u1) ) by A4, METRIC_1:11, METRIC_1:def 1;
then r <= sqrt ((((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2)) by Th7;
then A5: r * r <= (sqrt ((((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2))) ^2 by A3, XREAL_1:66;
( ((p `1) - (|[r1,s2]| `1)) ^2 >= 0 & ((p `2) - (|[r1,s2]| `2)) ^2 >= 0 ) by XREAL_1:63;
then A6: r ^2 <= (((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2) by A5, SQUARE_1:def 2;
( (Pitag_dist 2) . (u,u3) = dist (u,u3) & dist (u,u3) < r ) by A2, METRIC_1:11, METRIC_1:def 1;
then A10: sqrt ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) < r by Th7;
A11: ( ((p `1) - (|[s1,s2]| `1)) ^2 >= 0 & ((p `2) - (|[s1,s2]| `2)) ^2 >= 0 ) by XREAL_1:63;
then 0 <= sqrt ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) by SQUARE_1:def 2;
then (sqrt ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2))) ^2 < r * r by A10, XREAL_1:96;
then A12: (((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2) < r * r by A11, SQUARE_1:def 2;
( (Pitag_dist 2) . (u,u4) = dist (u,u4) & dist (u,u4) < r ) by A1, METRIC_1:11, METRIC_1:def 1;
then A13: sqrt ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) < r by Th7;
((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) + ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) = ((((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2)) + ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) ;
then A14: (r ^2) + ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) <= ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) + ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) by A6, XREAL_1:6;
A15: ( ((p `1) - (|[r1,r2]| `1)) ^2 >= 0 & ((p `2) - (|[r1,r2]| `2)) ^2 >= 0 ) by XREAL_1:63;
then 0 <= sqrt ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) by SQUARE_1:def 2;
then (sqrt ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2))) ^2 < r * r by A13, XREAL_1:96;
then (((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2) < r ^2 by A15, SQUARE_1:def 2;
then ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) + ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) < (r ^2) + (r ^2) by A12, XREAL_1:8;
then (r ^2) + ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) < (r ^2) + (r ^2) by A14, XXREAL_0:2;
then A16: (((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2) < ((r ^2) + (r ^2)) - (r ^2) by XREAL_1:20;
( ((p `1) - (|[s1,r2]| `1)) ^2 >= 0 & ((p `2) - (|[s1,r2]| `2)) ^2 >= 0 ) by XREAL_1:63;
then sqrt ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) < sqrt (r ^2) by A16, SQUARE_1:27;
then A17: sqrt ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) < r by A3, SQUARE_1:22;
dist (u,u2) = (Pitag_dist 2) . (u,u2) by METRIC_1:def 1
.= sqrt ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) by Th7 ;
hence ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) ) by A17, METRIC_1:11; :: thesis: verum

end;

end;