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

( 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