for CPS being proper CollSp
for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )