for CPS being CollProjectiveSpace
for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )