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:19;
hence LSeg (p,q) c= Cl S by A1, Th2; :: thesis: verum