let V be non trivial RealLinearSpace; :: thesis: ( ex u, v, u1, v1 being Element of V st
( ( for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) ) & ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) implies ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is up-3-dimensional & CS is at_most-3-dimensional ) )
assume ex u, v, u1, v1 being Element of V st
( ( for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) ) & ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) ; :: thesis: ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is up-3-dimensional & CS is at_most-3-dimensional )
then ( ex CS1 being CollProjectiveSpace st
( CS1 = ProjectiveSpace V & CS1 is up-3-dimensional ) & ex CS2 being CollProjectiveSpace st
( CS2 = ProjectiveSpace V & CS2 is at_most-3-dimensional ) ) by Th32, Th33;
hence ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is up-3-dimensional & CS is at_most-3-dimensional ) ; :: thesis: verum