for V being non trivial RealLinearSpace st ex x1, x2 being Element of (ProjectiveSpace V) st
( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) ) holds
for p, p1, q, q1 being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st
( p,p1,r are_collinear & q,q1,r are_collinear )