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;

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;

end;

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;(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

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;(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