let r, r1, r2, s1, s2 be Real; 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); ( |[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)
; ( |[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 A4:
not
|[r1,s2]| in Ball (
u,
r)
;
( |[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;
A7:
(
|[s1,r2]| `1 = s1 &
|[s1,r2]| `2 = r2 )
by EUCLID:52;
A8:
(
|[r1,r2]| `1 = r1 &
|[r1,r2]| `2 = r2 )
by EUCLID:52;
A9:
(
|[s1,s2]| `1 = s1 &
|[s1,s2]| `2 = s2 )
by EUCLID:52;
(
(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;
(
|[r1,s2]| `1 = r1 &
|[r1,s2]| `2 = s2 )
by EUCLID:52;
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: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;
verum end;