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:5;
now :: thesis: not p1 in LSeg (p,p2)
assume p1 in LSeg (p,p2) ; :: thesis: contradiction
then A4: (LSeg (p,p1)) \/ (LSeg (p1,p2)) = LSeg (p,p2) by TOPREAL1:5;
(LSeg (p,p1)) \/ (LSeg (p1,p2)) = LSeg (p1,p2) by A3, XBOOLE_1:7, XBOOLE_1:12;
hence contradiction by A1, A4, SPPOL_1:8; :: thesis: verum
end;
hence not p1 in LSeg (p,p2) ; :: thesis: verum