for CS being non empty CollStr holds
( CS is 2-dimensional CollProjectiveSpace iff ( CS is proper at_least_3rank CollSp & ( for p, p1, q, q1 being Element of CS ex r being Element of CS st
( p,p1,r are_collinear & q,q1,r are_collinear ) ) ) )