let A be non empty compact Subset of (TOP-REAL 2); :: thesis: for B being open Subset of (TOP-REAL 2) st A c= B holds
for p being Point of (TOP-REAL 2) st not p in B holds
dist p,B < dist p,A
let B be open Subset of (TOP-REAL 2); :: thesis: ( A c= B implies for p being Point of (TOP-REAL 2) st not p in B holds
dist p,B < dist p,A )
assume A1: A c= B ; :: thesis: for p being Point of (TOP-REAL 2) st not p in B holds
dist p,B < dist p,A
let p be Point of (TOP-REAL 2); :: thesis: ( not p in B implies dist p,B < dist p,A )
assume A2: not p in B ; :: thesis: dist p,B < dist p,A
A3: dist p,B <= dist p,A by A1, Th41;
assume dist p,B >= dist p,A ; :: thesis: contradiction
then A4: dist p,B = dist p,A by A3, XXREAL_0:1;
consider q being Point of (TOP-REAL 2) such that
A5: q in A and
A6: dist p,A = dist p,q by Th46;
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
then reconsider P = B as open Subset of (TopSpaceMetr (Euclid 2)) by PRE_TOPC:60;
reconsider a = q as Point of (Euclid 2) by TOPREAL3:13;
A7: a in P by A1, A5;
consider r being real number such that
A8: r > 0 and
A9: Ball a,r c= P by A1, A5, TOPMETR:22;
reconsider r = r as Element of REAL by XREAL_0:def 1;
set s = r / (2 * (dist p,q));
set q' = ((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p);
A10: dist p,q > 0 by A2, A7, Th22;
then A11: 2 * (dist p,q) > 0 by XREAL_1:131;
then A12: 0 < r / (2 * (dist p,q)) by A8, XREAL_1:141;
dist q,(((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p)) = ((1 * r) / (2 * (dist p,q))) * (dist p,q) by Th28, A11, A8
.= ((r / 2) / ((dist p,q) / 1)) * (dist p,q) by XCMPLX_1:85
.= r / 2 by A10, XCMPLX_1:88 ;
then A13: dist q,(((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p)) < r / 1 by A8, XREAL_1:78;
ex p1, q1 being Point of (Euclid 2) st
( p1 = q & q1 = ((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p) & dist q,(((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p)) = dist p1,q1 ) by TOPREAL6:def 1;
then A14: ((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p) in Ball a,r by A13, METRIC_1:12;

now

assume A15: r > dist p,q ; :: thesis: contradiction
ex p1, q1 being Point of (Euclid 2) st
( p1 = p & q1 = q & dist p,q = dist p1,q1 ) by TOPREAL6:def 1;
then p in Ball a,r by A15, METRIC_1:12;
hence contradiction by A2, A9; :: thesis: verum

end;

then 1 * r < 2 * (dist p,q) by A8, XREAL_1:100;
then r / (2 * (dist p,q)) < 1 by A11, XREAL_1:193;
then A16: dist p,(((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p)) = (1 - (r / (2 * (dist p,q)))) * (dist p,q) by Th27;
1 - (r / (2 * (dist p,q))) < 1 - 0 by A12, XREAL_1:12;
hence contradiction by A4, A6, A9, A14, Th50, A10, A16, XREAL_1:159; :: thesis: verum