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 that
A1: ( p <> p1 & p <> p2 ) and
A2: p in LSeg p1,p2 ; :: thesis: not p1 in LSeg p,p2
A3: (LSeg p1,p) \/ (LSeg p,p2) = LSeg p1,p2 by A2, TOPREAL1:11;

now

assume p1 in LSeg p,p2 ; :: thesis: contradiction
then A4: (LSeg p,p1) \/ (LSeg p1,p2) = LSeg p,p2 by TOPREAL1:11;
(LSeg p,p1) \/ (LSeg p1,p2) = LSeg p1,p2 by A3, XBOOLE_1:7, XBOOLE_1:12;
hence contradiction by A1, A4, SPPOL_1:25; :: thesis: verum

end;

hence not p1 in LSeg p,p2 ; :: thesis: verum