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:13;
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:60;
then consider r being real number such that
A5: r > 0 and
A6: Ball (x,r) c= P by A3, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A7: r / 2 > 0 by A5, XREAL_1:141;
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:13;
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:141;
then A9: 0 < min ((r / 2),((dist (x,y)) / 2)) by A7, XXREAL_0:21;
( (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p = (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a & ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q = ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b ) by EUCLID:69;
then A10: z = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b) by EUCLID:68;
dist (x,z) = |.(x9 - z9).| by SPPOL_1:20
.= |.((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 A10, RVSUM_1:60
.= |.(((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:74
.= |.(((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:71
.= |.(((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:72
.= |.((((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:71
.= |.((((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:71
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + ((- 1) * b))).| by RVSUM_1:73
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + (- b))).| by RVSUM_1:76
.= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a - b)).| by RVSUM_1:52
.= (abs ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * |.u.| by EUCLID:14
.= ((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:20
.= min ((r / 2),((dist (x,y)) / 2)) by A8, XCMPLX_1:88 ;
then A11: dist (x,z) <= r / 2 by XXREAL_0:17;
r / 2 < r / 1 by A5, XREAL_1:78;
then dist (x,z) < r by A11, XXREAL_0:2;
then A12: z in Ball (x,r) by METRIC_1:12;
A13: ((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 EUCLID:37
.= p by EUCLID:33 ;
( min ((r / 2),((dist (x,y)) / 2)) <= (dist (x,y)) / 2 & (dist (x,y)) / 2 < (dist (x,y)) / 1 ) by A8, XREAL_1:78, XXREAL_0:17;
then A14: 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:191;
then A15: ((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;
A16: ((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 EUCLID:37
.= q by EUCLID:33 ;
A17: 1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) <> 0 by A9, A14, XREAL_1:191;

A18: now

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 A16, EUCLID:52
.= (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p by EUCLID:52 ;
hence contradiction by A1, A17, EUCLID:38; :: thesis: verum

end;

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

now

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 A13, EUCLID:52
.= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q by EUCLID:52 ;
hence contradiction by A1, A19, EUCLID:38; :: 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 A18, 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 A15, XBOOLE_0:def 5;
hence (LSeg (p,q)) \ {p,q} meets G by A6, A12, XBOOLE_0:3; :: thesis: verum

end;

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