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, Th28;
A6:
not p2 in LSeg p,p1
by A2, A3, Th28;
per cases
( p1 in LSeg q,p2 or p2 in LSeg q,p1 )
by A1, A4, Th26, Th27;
suppose A7:
p1 in LSeg q,
p2
;
:: thesis: ( p1 in LSeg q,p or p2 in LSeg q,p )then A8:
(LSeg q,p1) \/ (LSeg p1,p2) = LSeg q,
p2
by TOPREAL1:11;
p in (LSeg q,p1) \/ (LSeg p1,p2)
by A2, XBOOLE_0:def 3;
then
(LSeg q,p) \/ (LSeg p,p2) = LSeg q,
p2
by A8, TOPREAL1:11;
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 )then A10:
(LSeg q,p2) \/ (LSeg p1,p2) = LSeg q,
p1
by TOPREAL1:11;
p in (LSeg q,p2) \/ (LSeg p1,p2)
by A2, XBOOLE_0:def 3;
then
(LSeg q,p) \/ (LSeg p,p1) = LSeg q,
p1
by A10, TOPREAL1:11;
hence
(
p1 in LSeg q,
p or
p2 in LSeg q,
p )
by A6, A9, XBOOLE_0:def 3;
:: thesis: verum end;