let r1, s1, s2, r2, r be real number ; :: thesis: for u being Point of (Euclid 2) st r1 <> s1 & s2 <> r2 & |[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 <> s1 & s2 <> r2 & |[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 A1:
( r1 <> s1 & s2 <> r2 & |[r1,r2]| in Ball u,r & |[s1,s2]| in Ball u,r )
; :: thesis: ( |[r1,s2]| in Ball u,r or |[s1,r2]| in Ball u,r )
then A2:
r > 0
by TBSP_1:17;
per cases
( |[r1,s2]| in Ball u,r or not |[r1,s2]| in Ball u,r )
;
suppose A3:
not
|[r1,s2]| in Ball u,
r
;
:: thesis: ( |[r1,s2]| in Ball u,r or |[s1,r2]| in Ball u,r )set p1 =
|[r1,s2]|;
set p2 =
|[s1,r2]|;
set p3 =
|[s1,s2]|;
set p4 =
|[r1,r2]|;
A4:
(
|[r1,s2]| `1 = r1 &
|[r1,s2]| `2 = s2 &
|[s1,r2]| `1 = s1 &
|[s1,r2]| `2 = r2 &
|[s1,s2]| `1 = s1 &
|[s1,s2]| `2 = s2 &
|[r1,r2]| `1 = r1 &
|[r1,r2]| `2 = r2 )
by EUCLID:56;
reconsider u1 =
|[r1,s2]|,
u2 =
|[s1,r2]|,
u3 =
|[s1,s2]|,
u4 =
|[r1,r2]| as
Point of
(Euclid 2) by EUCLID:25;
reconsider p =
u as
Point of
(TOP-REAL 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 );
(
((p `1 ) - (|[r1,s2]| `1 )) ^2 >= 0 &
((p `2 ) - (|[r1,s2]| `2 )) ^2 >= 0 )
by XREAL_1:65;
then A5:
0 + 0 <= (((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 )
;
(
((p `1 ) - (|[r1,r2]| `1 )) ^2 >= 0 &
((p `2 ) - (|[r1,r2]| `2 )) ^2 >= 0 )
by XREAL_1:65;
then A6:
0 + 0 <= (((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 )
;
then A7:
(
0 <= sqrt ((((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 )) &
((p `1 ) - (|[s1,s2]| `1 )) ^2 >= 0 &
((p `2 ) - (|[s1,s2]| `2 )) ^2 >= 0 )
by SQUARE_1:def 4, XREAL_1:65;
then A8:
0 + 0 <= (((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 )
;
then A9:
(
0 <= sqrt ((((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 )) &
((p `1 ) - (|[s1,r2]| `1 )) ^2 >= 0 &
((p `2 ) - (|[s1,r2]| `2 )) ^2 >= 0 )
by SQUARE_1:def 4, XREAL_1:65;
then A10:
0 + 0 <= (((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 )
;
A11:
(Pitag_dist 2) . u,
u1 = dist u,
u1
by METRIC_1:def 1;
r <= dist u,
u1
by A3, METRIC_1:12;
then
r <= sqrt ((((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 ))
by A11, Th12;
then
r * r <= (sqrt ((((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 ))) ^2
by A2, XREAL_1:68;
then A12:
r ^2 <= (((p `1 ) - (|[r1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,s2]| `2 )) ^2 )
by A5, SQUARE_1:def 4;
A13:
((((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 A4;
A14:
(Pitag_dist 2) . u,
u4 = dist u,
u4
by METRIC_1:def 1;
dist u,
u4 < r
by A1, METRIC_1:12;
then
sqrt ((((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 )) < r
by A14, Th12;
then
(sqrt ((((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 ))) ^2 < r * r
by A7, XREAL_1:98;
then A15:
(((p `1 ) - (|[r1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[r1,r2]| `2 )) ^2 ) < r ^2
by A6, SQUARE_1:def 4;
A16:
(Pitag_dist 2) . u,
u3 = dist u,
u3
by METRIC_1:def 1;
dist u,
u3 < r
by A1, METRIC_1:12;
then
sqrt ((((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 )) < r
by A16, Th12;
then
(sqrt ((((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 ))) ^2 < r * r
by A9, XREAL_1:98;
then
(((p `1 ) - (|[s1,s2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,s2]| `2 )) ^2 ) < r * r
by A8, SQUARE_1:def 4;
then A17:
((((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 A15, XREAL_1:10;
(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 A12, A13, XREAL_1:8;
then
(r ^2 ) + ((((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 )) < (r ^2 ) + (r ^2 )
by A17, XXREAL_0:2;
then
(((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 ) < ((r ^2 ) + (r ^2 )) - (r ^2 )
by XREAL_1:22;
then
sqrt ((((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 )) < sqrt (r ^2 )
by A10, SQUARE_1:95;
then A18:
sqrt ((((p `1 ) - (|[s1,r2]| `1 )) ^2 ) + (((p `2 ) - (|[s1,r2]| `2 )) ^2 )) < r
by A2, 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 A18, METRIC_1:12;
:: thesis: verum end;