let p, q, w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: ( w1 in (LSeg p,q) \ {p,q} & w2 in (LSeg p,q) \ {p,q} implies LSeg w1,w2 c= (LSeg p,q) \ {p,q} )
set P = (LSeg p,q) \ {p,q};
assume A1: ( w1 in (LSeg p,q) \ {p,q} & w2 in (LSeg p,q) \ {p,q} ) ; :: thesis: LSeg w1,w2 c= (LSeg p,q) \ {p,q}
then A2: ( w1 in LSeg p,q & w2 in LSeg p,q ) by XBOOLE_0:def 5;
( not w1 in {p,q} & not w2 in {p,q} ) by A1, XBOOLE_0:def 5;
then ( w1 <> p & w2 <> p & w1 <> q & w2 <> q ) by TARSKI:def 2;
then ( not p in LSeg w1,w2 & not q in LSeg w1,w2 ) by A2, SPPOL_1:24, TOPREAL1:12;
then LSeg w1,w2 misses {p,q} by ZFMISC_1:57;
hence LSeg w1,w2 c= (LSeg p,q) \ {p,q} by A2, TOPREAL1:12, XBOOLE_1:86; :: thesis: verum