for CPS being CollProjectiveSpace
for a, b, c, d, p being POINT of (IncProjSp_of CPS)
for P, Q, M, N being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q )