for PCPP being CollProjectiveSpace
for p, q being Element of PCPP st p <> q holds
ex r being Element of PCPP st not p,q,r are_collinear