let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q implies Cl ((LSeg p,q) \ {p,q}) = LSeg p,q )
assume A1: p <> q ; :: thesis: Cl ((LSeg p,q) \ {p,q}) = LSeg p,q
Cl ((LSeg p,q) \ {p,q}) c= Cl (LSeg p,q) by PRE_TOPC:49, XBOOLE_1:36;
hence Cl ((LSeg p,q) \ {p,q}) c= LSeg p,q by PRE_TOPC:52; :: according to XBOOLE_0:def 10 :: thesis: LSeg p,q c= Cl ((LSeg p,q) \ {p,q})
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in LSeg p,q or e in Cl ((LSeg p,q) \ {p,q}) )
assume A2: e in LSeg p,q ; :: thesis: e in Cl ((LSeg p,q) \ {p,q})
( p in LSeg p,q & q in LSeg p,q ) by RLTOPSP1:69;
then {p,q} c= LSeg p,q by ZFMISC_1:38;
then LSeg p,q = ((LSeg p,q) \ {p,q}) \/ {p,q} by XBOOLE_1:45;
then A3: ( e in (LSeg p,q) \ {p,q} or e in {p,q} ) by A2, XBOOLE_0:def 3;

per cases ( e in (LSeg p,q) \ {p,q} or e = p or e = q ) by A3, TARSKI:def 2;

suppose A4: e in (LSeg p,q) \ {p,q} ; :: thesis: e in Cl ((LSeg p,q) \ {p,q})

(LSeg p,q) \ {p,q} c= Cl ((LSeg p,q) \ {p,q}) by PRE_TOPC:48;
hence e in Cl ((LSeg p,q) \ {p,q}) by A4; :: thesis: verum

end;

suppose ( e = p or e = q ) ; :: thesis: e in Cl ((LSeg p,q) \ {p,q})

hence e in Cl ((LSeg p,q) \ {p,q}) by A1, Th6; :: thesis: verum

end;

end;