let p, p1, p2, q be Point of (TOP-REAL 2); ( 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 ) )
; ( 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)
;
( 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;
verum end; suppose A9:
p2 in LSeg (
q,
p1)
;
( 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;
verum end;