let V be non trivial RealLinearSpace; :: thesis: ( ex u, v, w being Element of V st

( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) implies ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is 2-dimensional ) )

given u, v, w being Element of V such that A1: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds

( a = 0 & b = 0 & c = 0 ) and

A2: for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ; :: thesis: ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is 2-dimensional )

reconsider V9 = V as up-3-dimensional RealLinearSpace by A1, Def6;

take ProjectiveSpace V9 ; :: thesis: ( ProjectiveSpace V9 = ProjectiveSpace V & ProjectiveSpace V9 is 2-dimensional )

ex x1, x2 being Element of (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) ) by A1, A2, Th27;

then for p, p1, q, q1 being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st

( p,p1,r are_collinear & q,q1,r are_collinear ) by Th28;

hence ( ProjectiveSpace V9 = ProjectiveSpace V & ProjectiveSpace V9 is 2-dimensional ) ; :: thesis: verum

( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds

( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) implies ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is 2-dimensional ) )

given u, v, w being Element of V such that A1: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds

( a = 0 & b = 0 & c = 0 ) and

A2: for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ; :: thesis: ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is 2-dimensional )

reconsider V9 = V as up-3-dimensional RealLinearSpace by A1, Def6;

take ProjectiveSpace V9 ; :: thesis: ( ProjectiveSpace V9 = ProjectiveSpace V & ProjectiveSpace V9 is 2-dimensional )

ex x1, x2 being Element of (ProjectiveSpace V) st

( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st

( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) ) by A1, A2, Th27;

then for p, p1, q, q1 being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st

( p,p1,r are_collinear & q,q1,r are_collinear ) by Th28;

hence ( ProjectiveSpace V9 = ProjectiveSpace V & ProjectiveSpace V9 is 2-dimensional ) ; :: thesis: verum