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 A4: LSeg p1,p2 meets LSeg p3,p4 by XBOOLE_0:4;
p in LSeg p3,p4 by A3, XBOOLE_0:def 4;
then (LSeg p3,p) \/ (LSeg p,p4) = LSeg p3,p4 by TOPREAL1:11;
then A5: LSeg p3,p c= LSeg p3,p4 by XBOOLE_1:7;
A6: p1 in LSeg p1,p2 by RLTOPSP1:69;
A7: p2 in LSeg p1,p2 by RLTOPSP1:69;
A8: p3 in LSeg p3,p4 by RLTOPSP1:69;

A9: now

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:37;
hence p2 `1 = p3 `1 by A4, Th25; :: thesis: verum

end;

A10: now

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:36;
hence p2 `2 = p3 `2 by A4, SPRECT_3:21; :: thesis: verum

end;

now

assume A11: ( p <> p1 & p <> p2 & p <> p3 ) ; :: thesis: contradiction
A12: p in LSeg p1,p2 by A3, XBOOLE_0:def 4;

A13: now

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, A11, TARSKI:def 1; :: thesis: verum

end;

now

per cases ( p1 in LSeg p3,p or p2 in LSeg p3,p ) by A1, A9, A10, A11, A12, A13, Th29;

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

then p1 in (LSeg p1,p2) /\ (LSeg p3,p4) by A5, A6, XBOOLE_0:def 4;
hence contradiction by A2, A11, TARSKI:def 1; :: thesis: verum

end;

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

then p2 in (LSeg p1,p2) /\ (LSeg p3,p4) by A5, A7, XBOOLE_0:def 4;
hence contradiction by A2, A11, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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