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