let S be Subset of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg p,q) \ {p,q} c= S holds
LSeg p,q c= Cl S
let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q & (LSeg p,q) \ {p,q} c= S implies LSeg p,q c= Cl S )
assume A1: p <> q ; :: thesis: ( not (LSeg p,q) \ {p,q} c= S or LSeg p,q c= Cl S )
assume (LSeg p,q) \ {p,q} c= S ; :: thesis: LSeg p,q c= Cl S
then Cl ((LSeg p,q) \ {p,q}) c= Cl S by PRE_TOPC:49;
hence LSeg p,q c= Cl S by A1, Th7; :: thesis: verum