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)
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:30;
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)
assume A3: dist (p,B) >= dist (p,A) ; :: thesis: contradiction
dist (p,B) <= dist (p,A) by A1, Th41;
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;
reconsider a = q as Point of (Euclid 2) by TOPREAL3:8;
consider r being Real such that
A7: r > 0 and
A8: Ball (a,r) c= P by A1, A5, TOPMETR:15;
reconsider r = r as Element of REAL by XREAL_0:def 1;
set s = r / (2 * (dist (p,q)));
set q9 = ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p);
a in P by A1, A5;
then A9: dist (p,q) > 0 by A2, Th22;
then A10: 2 * (dist (p,q)) > 0 by XREAL_1:129;
then 0 < r / (2 * (dist (p,q))) by A7, XREAL_1:139;
then A11: 1 - (r / (2 * (dist (p,q)))) < 1 - 0 by XREAL_1:10;
A12: 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;
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 A7, A9, Th28
.= ((r / 2) / ((dist (p,q)) / 1)) * (dist (p,q)) by XCMPLX_1:84
.= r / 2 by A9, XCMPLX_1:87 ;
then dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) < r / 1 by A7, XREAL_1:76;
then A13: ((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p) in Ball (a,r) by A12, METRIC_1:11;

now :: thesis: not r > dist (p,q)

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

end;

then 1 * r < 2 * (dist (p,q)) by A7, XREAL_1:98;
then r / (2 * (dist (p,q))) < 1 by A10, XREAL_1:191;
then 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;
hence contradiction by A4, A6, A8, A9, A13, A11, Th50, XREAL_1:157; :: thesis: verum