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:19, XBOOLE_1:36;
hence Cl ((LSeg (p,q)) \ {p,q}) c= LSeg (p,q) by PRE_TOPC:22; :: according to XBOOLE_0:def 10 :: thesis: LSeg (p,q) c= Cl ((LSeg (p,q)) \ {p,q})
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in LSeg (p,q) or e in Cl ((LSeg (p,q)) \ {p,q}) )
( p in LSeg (p,q) & q in LSeg (p,q) ) by RLTOPSP1:68;
then {p,q} c= LSeg (p,q) by ZFMISC_1:32;
then A2: LSeg (p,q) = ((LSeg (p,q)) \ {p,q}) \/ {p,q} by XBOOLE_1:45;
assume e in LSeg (p,q) ; :: thesis: e in Cl ((LSeg (p,q)) \ {p,q})
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:18;
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, Th1; :: thesis: verum
end;
end;