let r1, r2, r, s1, s2 be real number ; :: 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:17;

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:25;
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:25;
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:12, METRIC_1:def 1;
then r <= sqrt ((((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 )) by Th12;
then A5: r * r <= (sqrt ((((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 ))) ^2 by A3, XREAL_1:68;
( ((p `1 ) - (|[r1,s2]| `1 )) ^2 >= 0 & ((p `2 ) - (|[r1,s2]| `2 )) ^2 >= 0 ) by XREAL_1:65;
then A6: r ^2 <= (((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 ) by A5, SQUARE_1:def 4;
A7: ( |[s1,r2]| `1 = s1 & |[s1,r2]| `2 = r2 ) by EUCLID:56;
A8: ( |[r1,r2]| `1 = r1 & |[r1,r2]| `2 = r2 ) by EUCLID:56;
A9: ( |[s1,s2]| `1 = s1 & |[s1,s2]| `2 = s2 ) by EUCLID:56;
( (Pitag_dist 2) . u,u3 = dist u,u3 & dist u,u3 < r ) by A2, METRIC_1:12, METRIC_1:def 1;
then A10: sqrt ((((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 )) < r by Th12;
A11: ( ((p `1 ) - (|[s1,s2]| `1 )) ^2 >= 0 & ((p `2 ) - (|[s1,s2]| `2 )) ^2 >= 0 ) by XREAL_1:65;
then 0 <= sqrt ((((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 )) by SQUARE_1:def 4;
then (sqrt ((((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 ))) ^2 < r * r by A10, XREAL_1:98;
then A12: (((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 ) < r * r by A11, SQUARE_1:def 4;
( (Pitag_dist 2) . u,u4 = dist u,u4 & dist u,u4 < r ) by A1, METRIC_1:12, METRIC_1:def 1;
then A13: sqrt ((((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 )) < r by Th12;
( |[r1,s2]| `1 = r1 & |[r1,s2]| `2 = s2 ) by EUCLID:56;
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 )) = ((((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 )) + ((((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 )) by A7, A9, A8;
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:8;
A15: ( ((p `1 ) - (|[r1,r2]| `1 )) ^2 >= 0 & ((p `2 ) - (|[r1,r2]| `2 )) ^2 >= 0 ) by XREAL_1:65;
then 0 <= sqrt ((((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 )) by SQUARE_1:def 4;
then (sqrt ((((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 ))) ^2 < r * r by A13, XREAL_1:98;
then (((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 ) < r ^2 by A15, SQUARE_1:def 4;
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:10;
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:22;
( ((p `1 ) - (|[s1,r2]| `1 )) ^2 >= 0 & ((p `2 ) - (|[s1,r2]| `2 )) ^2 >= 0 ) by XREAL_1:65;
then sqrt ((((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 )) < sqrt (r ^2 ) by A16, SQUARE_1:95;
then A17: sqrt ((((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 )) < r by A3, SQUARE_1:89;
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 Th12 ;
hence ( |[r1,s2]| in Ball u,r or |[s1,r2]| in Ball u,r ) by A17, METRIC_1:12; :: thesis: verum

end;

end;