for CPS being CollProjectiveSpace st ( for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of CPS st
( p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear ) ) holds
for a being POINT of (IncProjSp_of CPS)
for M, N being LINE of (IncProjSp_of CPS) ex b, c being POINT of (IncProjSp_of CPS) ex S being LINE of (IncProjSp_of CPS) st
( a on S & b on S & c on S & b on M & c on N )