for CPS being CollProjectiveSpace st ( for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st
( a9,b9,p9 are_collinear & c9,d9,p9 are_collinear ) ) holds
for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )