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:7, TOPREAL1:6;
not q in LSeg (w1,w2)
by A3, A4, A9, A10, SPPOL_1:7, TOPREAL1:6;
then
LSeg (w1,w2) misses {p,q}
by A11, ZFMISC_1:51;
hence
LSeg (w1,w2) c= (LSeg (p,q)) \ {p,q}
by A3, A4, TOPREAL1:6, XBOOLE_1:86; verum