let p1, p2, p3, p4, p be Point of (TOP-REAL 2); ( ( ( p1 `1 = p2 `1 & p3 `1 = p4 `1 ) or ( p1 `2 = p2 `2 & p3 `2 = p4 `2 ) ) & (LSeg (p1,p2)) /\ (LSeg (p3,p4)) = {p} & not p = p1 & not p = p2 implies p = p3 )
assume that
A1:
( ( p1 `1 = p2 `1 & p3 `1 = p4 `1 ) or ( p1 `2 = p2 `2 & p3 `2 = p4 `2 ) )
and
A2:
(LSeg (p1,p2)) /\ (LSeg (p3,p4)) = {p}
; ( p = p1 or p = p2 or p = p3 )
A3:
p in (LSeg (p1,p2)) /\ (LSeg (p3,p4))
by A2, TARSKI:def 1;
then
p in LSeg (p3,p4)
by XBOOLE_0:def 4;
then
(LSeg (p3,p)) \/ (LSeg (p,p4)) = LSeg (p3,p4)
by TOPREAL1:5;
then A4:
LSeg (p3,p) c= LSeg (p3,p4)
by XBOOLE_1:7;
A5:
LSeg (p1,p2) meets LSeg (p3,p4)
by A3;
A8:
p3 in LSeg (p3,p4)
by RLTOPSP1:68;
A9:
p2 in LSeg (p1,p2)
by RLTOPSP1:68;
A10:
p1 in LSeg (p1,p2)
by RLTOPSP1:68;
now ( p <> p1 & p <> p2 implies not p <> p3 )A11:
p in LSeg (
p1,
p2)
by A3, XBOOLE_0:def 4;
assume that A12:
p <> p1
and A13:
p <> p2
and A14:
p <> p3
;
contradictionhence
contradiction
;
verum end;
hence
( p = p1 or p = p2 or p = p3 )
; verum