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 is_collinear & q,q1,r is_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 is_collinear & q,q1,r is_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 is_collinear & q,q1,r is_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 is_collinear & q,q1,r is_collinear ) ; :: thesis: CS is 2-dimensional CollProjectiveSpace
CS is Vebleian

proof

let p, p1, p2, r, r1 be Element of CS; :: according to ANPROJ_2:def 9 :: thesis: ( p,p1,r is_collinear & p1,p2,r1 is_collinear implies ex r2 being Element of CS st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear ) )
assume that
p,p1,r is_collinear and
p1,p2,r1 is_collinear ; :: thesis: ex r2 being Element of CS st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
thus ex r2 being Element of CS st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear ) by A2; :: thesis: verum

end;

hence CS is 2-dimensional CollProjectiveSpace by A1, A2, Def14; :: thesis: verum