for CPS being CollProjectiveSpace st ex p, p1, r, r1 being Point of CPS st
for s being Point of CPS holds
( not p,p1,s are_collinear or not r,r1,s are_collinear ) holds
ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )