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;

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)

hence
not p1 in LSeg (p,p2)
; :: thesis: verumassume
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;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