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

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
X: 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)) ;
reconsider x = p, y = q as Point of (Euclid 2) by TOPREAL3:13;
P is open by A2, X, PRE_TOPC:60;
then consider r being real number such that
A4: r > 0 and
A5: Ball x,r c= P by A2, A3, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
set t = min (r / 2),((dist x,y) / 2);
set s = (min (r / 2),((dist x,y) / 2)) / (dist x,y);
A6: r / 2 > 0 by A4, XREAL_1:141;
A7: 0 < dist x,y by A1, SUB_METR:2;
then 0 < (dist x,y) / 2 by XREAL_1:141;
then A8: 0 < min (r / 2),((dist x,y) / 2) by A6, XXREAL_0:21;
then A9: 0 < (min (r / 2),((dist x,y) / 2)) / (dist x,y) by A7, XREAL_1:141;
A10: min (r / 2),((dist x,y) / 2) <= (dist x,y) / 2 by XXREAL_0:17;
(dist x,y) / 2 < (dist x,y) / 1 by A7, XREAL_1:78;
then A11: min (r / 2),((dist x,y) / 2) < dist x,y by A10, XXREAL_0:2;
then A12: (min (r / 2),((dist x,y) / 2)) / (dist x,y) < 1 by A8, XREAL_1:191;
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;
A13: ((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 A9, A12;
A14: ((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 ;

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

end;

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 A8, A11, XREAL_1:191;

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;

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 A15, TARSKI:def 2;
then A18: ((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 A13, XBOOLE_0:def 5;
reconsider x' = x, y' = y, z' = z as Element of REAL 2 ;
reconsider a = x', b = y' as Element of 2 -tuples_on REAL ;
reconsider u = a - b as Element of REAL 2 ;
Y: (1 - ((min (r / 2),((dist x,y) / 2)) / (dist x,y))) * p = (1 - ((min (r / 2),((dist x,y) / 2)) / (dist x,y))) * a by EUCLID:69;
((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 X: 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 Y, EUCLID:68;
dist x,z = |.(x' - z').| 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 X, 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 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 A7, XCMPLX_1:88 ;
then A19: dist x,z <= r / 2 by XXREAL_0:17;
r / 2 < r / 1 by A4, XREAL_1:78;
then dist x,z < r by A19, XXREAL_0:2;
then z in Ball x,r by METRIC_1:12;
hence (LSeg p,q) \ {p,q} meets G by A5, A18, XBOOLE_0:3; :: thesis: verum

end;

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