for CPS being proper CollSp
for a, b, c being POINT of (IncProjSp_of CPS)
for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )