let p1, p2, p3, p4, p be Point of (TOP-REAL 2); :: thesis: ( ( ( 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} ; :: thesis: ( 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;

A9: p2 in LSeg (p1,p2) by RLTOPSP1:68;

A10: p1 in LSeg (p1,p2) by RLTOPSP1:68;

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} ; :: thesis: ( 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;

A6: now :: thesis: ( p1 `2 = p2 `2 & p3 `2 = p4 `2 implies p2 `2 = p3 `2 )

assume
( p1 `2 = p2 `2 & p3 `2 = p4 `2 )
; :: thesis: p2 `2 = p3 `2

then ( LSeg (p1,p2) is horizontal & LSeg (p3,p4) is horizontal ) by SPPOL_1:15;

hence p2 `2 = p3 `2 by A5, SPRECT_3:9; :: thesis: verum

end;then ( LSeg (p1,p2) is horizontal & LSeg (p3,p4) is horizontal ) by SPPOL_1:15;

hence p2 `2 = p3 `2 by A5, SPRECT_3:9; :: thesis: verum

A7: now :: thesis: ( p1 `1 = p2 `1 & p3 `1 = p4 `1 implies p2 `1 = p3 `1 )

A8:
p3 in LSeg (p3,p4)
by RLTOPSP1:68;assume
( p1 `1 = p2 `1 & p3 `1 = p4 `1 )
; :: thesis: p2 `1 = p3 `1

then ( LSeg (p1,p2) is vertical & LSeg (p3,p4) is vertical ) by SPPOL_1:16;

hence p2 `1 = p3 `1 by A5, Th24; :: thesis: verum

end;then ( LSeg (p1,p2) is vertical & LSeg (p3,p4) is vertical ) by SPPOL_1:16;

hence p2 `1 = p3 `1 by A5, Th24; :: thesis: verum

A9: p2 in LSeg (p1,p2) by RLTOPSP1:68;

A10: p1 in LSeg (p1,p2) by RLTOPSP1:68;

now :: thesis: ( p <> p1 & p <> p2 implies not p <> p3 )

hence
( p = p1 or p = p2 or p = p3 )
; :: thesis: verumA11:
p in LSeg (p1,p2)
by A3, XBOOLE_0:def 4;

assume that

A12: p <> p1 and

A13: p <> p2 and

A14: p <> p3 ; :: thesis: contradiction

end;assume that

A12: p <> p1 and

A13: p <> p2 and

A14: p <> p3 ; :: thesis: contradiction

A15: now :: thesis: not p3 in LSeg (p1,p2)

assume
p3 in LSeg (p1,p2)
; :: thesis: contradiction

then p3 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by A8, XBOOLE_0:def 4;

hence contradiction by A2, A14, TARSKI:def 1; :: thesis: verum

end;then p3 in (LSeg (p1,p2)) /\ (LSeg (p3,p4)) by A8, XBOOLE_0:def 4;

hence contradiction by A2, A14, TARSKI:def 1; :: thesis: verum

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( p1 in LSeg (p3,p) or p2 in LSeg (p3,p) )
by A1, A7, A6, A12, A13, A11, A15, Th28;

end;

suppose
p1 in LSeg (p3,p)
; :: thesis: contradiction

then
p1 in (LSeg (p1,p2)) /\ (LSeg (p3,p4))
by A4, A10, XBOOLE_0:def 4;

hence contradiction by A2, A12, TARSKI:def 1; :: thesis: verum

end;hence contradiction by A2, A12, TARSKI:def 1; :: thesis: verum

suppose
p2 in LSeg (p3,p)
; :: thesis: contradiction

then
p2 in (LSeg (p1,p2)) /\ (LSeg (p3,p4))
by A4, A9, XBOOLE_0:def 4;

hence contradiction by A2, A13, TARSKI:def 1; :: thesis: verum

end;hence contradiction by A2, A13, TARSKI:def 1; :: thesis: verum