for CPS being proper CollSp
for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS)
for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )