let CS be non empty CollStr ; :: thesis: ( 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 ) ) ) )
thus ( CS is 2-dimensional CollProjectiveSpace implies ( 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 ) ) ) ) by Def14; :: thesis: ( 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 ) ) implies CS is 2-dimensional CollProjectiveSpace )
assume that
A1: CS is proper at_least_3rank CollSp and
A2: 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 ) ; :: thesis: CS is 2-dimensional CollProjectiveSpace
CS is Vebleian by A2;
hence CS is 2-dimensional CollProjectiveSpace by A1, A2, Def14; :: thesis: verum