for V being non trivial RealLinearSpace st ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank & ex p, q1, q2 being Element of (ProjectiveSpace V) st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) ) holds
ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )