let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p <> p1 & p <> p2 & p in LSeg p1,p2 implies not p1 in LSeg p,p2 )
assume A1:
( p <> p1 & p <> p2 & p in LSeg p1,p2 )
; :: thesis: not p1 in LSeg p,p2
then A2:
(LSeg p1,p) \/ (LSeg p,p2) = LSeg p1,p2
by TOPREAL1:11;
now assume
p1 in LSeg p,
p2
;
:: thesis: contradictionthen A3:
(LSeg p,p1) \/ (LSeg p1,p2) = LSeg p,
p2
by TOPREAL1:11;
(LSeg p,p1) \/ (LSeg p1,p2) = LSeg p1,
p2
by A2, XBOOLE_1:7, XBOOLE_1:12;
hence
contradiction
by A1, A3, SPPOL_1:25;
:: thesis: verum end;
hence
not p1 in LSeg p,p2
; :: thesis: verum