let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q implies p in Cl ((LSeg (p,q)) \ {p,q}) )
assume A1: p <> q ; :: thesis: p in Cl ((LSeg (p,q)) \ {p,q})
for G being Subset of (TOP-REAL 2) st G is open & p in G holds
(LSeg (p,q)) \ {p,q} meets G

proof

reconsider x = p, y = q as Point of (Euclid 2) by TOPREAL3:8;
let G be Subset of (TOP-REAL 2); :: thesis: ( G is open & p in G implies (LSeg (p,q)) \ {p,q} meets G )
assume that
A2: G is open and
A3: p in G ; :: thesis: (LSeg (p,q)) \ {p,q} meets G
A4: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
then reconsider P = G as Subset of (TopSpaceMetr (Euclid 2)) ;
P is open by A2, A4, PRE_TOPC:30;
then consider r being Real such that
A5: r > 0 and
A6: Ball (x,r) c= P by A3, TOPMETR:15;
reconsider r = r as Real ;
A7: r / 2 > 0 by A5, XREAL_1:139;
set t = min ((r / 2),((dist (x,y)) / 2));
set s = (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y));
set pp = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q);
reconsider z = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) as Point of (Euclid 2) by TOPREAL3:8;
reconsider x9 = x, y9 = y, z9 = z as Element of REAL 2 ;
reconsider a = x9, b = y9 as Element of 2 -tuples_on REAL ;
reconsider u = a - b as Element of REAL 2 ;
A8: 0 < dist (x,y) by A1, METRIC_1:7;
then 0 < (dist (x,y)) / 2 by XREAL_1:139;
then A9: 0 < min ((r / 2),((dist (x,y)) / 2)) by A7, XXREAL_0:21;
dist (x,z) = |.(x9 - z9).| by SPPOL_1:5
.= |.((a - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:39
.= |.(((1 * a) - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:52
.= |.(((1 * a) + (((- 1) * (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:49
.= |.(((1 + (- (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))))) * a) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:50
.= |.((((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * a) + (((- 1) * ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * b)).| by RVSUM_1:49
.= |.((((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * a) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * ((- 1) * b))).| by RVSUM_1:49
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + ((- 1) * b))).| by RVSUM_1:51
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + (- b))).|
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a - b)).|
.= |.((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))).| * |.u.| by EUCLID:11
.= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * |.(a - b).| by A8, A9, ABSVALUE:def 1
.= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (dist (x,y)) by SPPOL_1:5
.= min ((r / 2),((dist (x,y)) / 2)) by A8, XCMPLX_1:87 ;
then A10: dist (x,z) <= r / 2 by XXREAL_0:17;
r / 2 < r / 1 by A5, XREAL_1:76;
then dist (x,z) < r by A10, XXREAL_0:2;
then A11: z in Ball (x,r) by METRIC_1:11;
A12: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * p) = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) + ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p by RLVECT_1:def 6
.= p by RLVECT_1:def 8 ;
( min ((r / 2),((dist (x,y)) / 2)) <= (dist (x,y)) / 2 & (dist (x,y)) / 2 < (dist (x,y)) / 1 ) by A8, XREAL_1:76, XXREAL_0:17;
then A13: min ((r / 2),((dist (x,y)) / 2)) < dist (x,y) by XXREAL_0:2;
then (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)) < 1 by A9, XREAL_1:189;
then A14: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in LSeg (p,q) by A8, A9;
A15: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) + ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q by RLVECT_1:def 6
.= q by RLVECT_1:def 8 ;
A16: 1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) <> 0 by A9, A13, XREAL_1:189;

A17: now :: thesis: not ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = q

assume ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = q ; :: thesis: contradiction
then (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q = (((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) by A15, RLVECT_4:1
.= (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p by RLVECT_4:1 ;
hence contradiction by A1, A16, RLVECT_1:36; :: thesis: verum

end;

A18: 0 < (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)) by A8, A9, XREAL_1:139;

now :: thesis: not ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = p

assume ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = p ; :: thesis: contradiction
then ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * p = (((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q)) - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) by A12, RLVECT_4:1
.= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q by RLVECT_4:1 ;
hence contradiction by A1, A18, RLVECT_1:36; :: thesis: verum

end;

then not ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in {p,q} by A17, TARSKI:def 2;
then ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in (LSeg (p,q)) \ {p,q} by A14, XBOOLE_0:def 5;
hence (LSeg (p,q)) \ {p,q} meets G by A6, A11, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl ((LSeg (p,q)) \ {p,q}) by TOPS_1:12; :: thesis: verum