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:60;
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:13;
consider r being real number such that
A7: r > 0 and
A8: 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 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:131;
then 0 < r / (2 * (dist p,q)) by A7, XREAL_1:141;
then A11: 1 - (r / (2 * (dist p,q))) < 1 - 0 by XREAL_1:12;
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:85
.= r / 2 by A9, XCMPLX_1:88 ;
then dist q,(((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p)) < r / 1 by A7, XREAL_1:78;
then A13: ((1 - (r / (2 * (dist p,q)))) * q) + ((r / (2 * (dist p,q))) * p) in Ball a,r by A12, METRIC_1:12;

now

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:12;
hence contradiction by A2, A8; :: thesis: verum

end;

then 1 * r < 2 * (dist p,q) by A7, XREAL_1:100;
then r / (2 * (dist p,q)) < 1 by A10, XREAL_1:193;
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:159; :: thesis: verum