let p, q, w1, w2 be Point of (TOP-REAL 2); JORDAN1:def 1 ( 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 that
A1:
w1 in (LSeg p,q) \ {p,q}
and
A2:
w2 in (LSeg p,q) \ {p,q}
; LSeg w1,w2 c= (LSeg p,q) \ {p,q}
A3:
w1 in LSeg p,q
by A1, XBOOLE_0:def 5;
A4:
w2 in LSeg p,q
by A2, XBOOLE_0:def 5;
A5:
not w1 in {p,q}
by A1, XBOOLE_0:def 5;
A6:
not w2 in {p,q}
by A2, XBOOLE_0:def 5;
A7:
w1 <> p
by A5, TARSKI:def 2;
A8:
w2 <> p
by A6, TARSKI:def 2;
A9:
w1 <> q
by A5, TARSKI:def 2;
A10:
w2 <> q
by A6, TARSKI:def 2;
A11:
not p in LSeg w1,w2
by A3, A4, A7, A8, SPPOL_1:24, TOPREAL1:12;
not q in LSeg w1,w2
by A3, A4, A9, A10, SPPOL_1:24, TOPREAL1:12;
then
LSeg w1,w2 misses {p,q}
by A11, ZFMISC_1:57;
hence
LSeg w1,w2 c= (LSeg p,q) \ {p,q}
by A3, A4, TOPREAL1:12, XBOOLE_1:86; verum