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;

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;

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

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;

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

now :: thesis: contradiction

per cases ( p1 in LSeg (p3,p) or p2 in LSeg (p3,p) ) by A1, A7, A6, A12, A13, A11, A15, Th28;

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;

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;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence ( p = p1 or p = p2 or p = p3 ) ; :: thesis: verum