for PCPP being CollProjectiveSpace
for a1, a2, b1, b2, o being Element of PCPP st not o,a1,a2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o <> b1 & o <> b2 holds
not o,b1,b2 are_collinear