let p, p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( not q in LSeg (p1,p2) & p in LSeg (p1,p2) & p <> p1 & p <> p2 & ( ( p1 `1 = p2 `1 & p2 `1 = q `1 ) or ( p1 `2 = p2 `2 & p2 `2 = q `2 ) ) & not p1 in LSeg (q,p) implies p2 in LSeg (q,p) )
assume that
A1: not q in LSeg (p1,p2) and
A2: p in LSeg (p1,p2) and
A3: ( p <> p1 & p <> p2 ) and
A4: ( ( p1 `1 = p2 `1 & p2 `1 = q `1 ) or ( p1 `2 = p2 `2 & p2 `2 = q `2 ) ) ; :: thesis: ( p1 in LSeg (q,p) or p2 in LSeg (q,p) )
A5: not p1 in LSeg (p,p2) by A2, A3, Th27;
A6: not p2 in LSeg (p,p1) by A2, A3, Th27;

per cases ( p1 in LSeg (q,p2) or p2 in LSeg (q,p1) ) by A1, A4, Th25, Th26;

suppose A7: p1 in LSeg (q,p2) ; :: thesis: ( p1 in LSeg (q,p) or p2 in LSeg (q,p) )

A8: p in (LSeg (q,p1)) \/ (LSeg (p1,p2)) by A2, XBOOLE_0:def 3;
(LSeg (q,p1)) \/ (LSeg (p1,p2)) = LSeg (q,p2) by A7, TOPREAL1:5;
then (LSeg (q,p)) \/ (LSeg (p,p2)) = LSeg (q,p2) by A8, TOPREAL1:5;
hence ( p1 in LSeg (q,p) or p2 in LSeg (q,p) ) by A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A9: p2 in LSeg (q,p1) ; :: thesis: ( p1 in LSeg (q,p) or p2 in LSeg (q,p) )

A10: p in (LSeg (q,p2)) \/ (LSeg (p1,p2)) by A2, XBOOLE_0:def 3;
(LSeg (q,p2)) \/ (LSeg (p1,p2)) = LSeg (q,p1) by A9, TOPREAL1:5;
then (LSeg (q,p)) \/ (LSeg (p,p1)) = LSeg (q,p1) by A10, TOPREAL1:5;
hence ( p1 in LSeg (q,p) or p2 in LSeg (q,p) ) by A6, A9, XBOOLE_0:def 3; :: thesis: verum

end;

end;