let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: for r, r1, r2, s1, s2 being Real
for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) holds
p in Ball (u,r)
let r, r1, r2, s1, s2 be Real; :: thesis: for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) holds
p in Ball (u,r)
let u be Point of (Euclid 2); :: thesis: ( u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) implies p in Ball (u,r) )
assume that
A1: u = p1 and
A2: p1 = |[r1,s1]| and
A3: p2 = |[r2,s2]| and
A4: p = |[r2,s1]| and
A5: p2 in Ball (u,r) ; :: thesis: p in Ball (u,r)
reconsider p19 = p1, p29 = p2, p9 = p as Element of REAL 2 by EUCLID:22;
reconsider r1 = r1, s1 = s1, r2 = r2, s2 = s2 as Real ;
A6: (Pitag_dist 2) . (p19,p29) = |.(p19 - p29).| by EUCLID:def 6;
p2 in { u6 where u6 is Element of (Euclid 2) : dist (u,u6) < r } by A5, METRIC_1:17;
then ex u5 being Point of (Euclid 2) st
( u5 = p2 & dist (u,u5) < r ) ;
then A7: |.(p19 - p29).| < r by A1, A6, METRIC_1:def 1;
reconsider up = p as Point of (Euclid 2) by EUCLID:22;
(Pitag_dist 2) . (p19,p9) = |.(p19 - p9).| by EUCLID:def 6;
then A8: dist (u,up) = |.(p19 - p9).| by A1, METRIC_1:def 1;
(s1 - s2) ^2 >= 0 by XREAL_1:63;
then sqrreal . (s1 - s2) >= 0 by RVSUM_1:def 2;
then A9: (sqrreal . (r1 - r2)) + 0 <= (sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2)) by XREAL_1:7;
p19 - p9 = p1 - p by EUCLID:69;
then p19 - p9 = <*(r1 - r2),(s1 - s1)*> by A2, A4, Th5;
then sqr (p19 - p9) = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s1))*> by FINSEQ_2:36;
then A10: Sum (sqr (p19 - p9)) = (sqrreal . (r1 - r2)) + (sqrreal . 0) by RVSUM_1:77
.= (sqrreal . (r1 - r2)) + (0 ^2) by RVSUM_1:def 2
.= sqrreal . (r1 - r2) ;
p19 - p29 = p1 - p2 by EUCLID:69;
then p19 - p29 = <*(r1 - r2),(s1 - s2)*> by A2, A3, Th5;
then sqr (p19 - p29) = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s2))*> by FINSEQ_2:36;
then A11: |.(p19 - p29).| = sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by RVSUM_1:77;
(r1 - r2) ^2 >= 0 by XREAL_1:63;
then sqrreal . (r1 - r2) >= 0 by RVSUM_1:def 2;
then |.(p19 - p9).| <= sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by A10, A9, SQUARE_1:26;
then |.(p19 - p9).| < r by A7, A11, XXREAL_0:2;
then p in { u6 where u6 is Element of (Euclid 2) : dist (u,u6) < r } by A8;
hence p in Ball (u,r) by METRIC_1:17; :: thesis: verum