let V be non trivial RealLinearSpace; :: thesis: ( V is up-3-dimensional implies ProjectiveSpace V is at_least_3rank )

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

( a = 0 & b = 0 & c = 0 ) ; :: according to ANPROJ_2:def 6 :: thesis: ProjectiveSpace V is at_least_3rank

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

( a = 0 & b = 0 & c = 0 ) ; :: according to ANPROJ_2:def 6 :: thesis: ProjectiveSpace V is at_least_3rank

now :: thesis: for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 )

hence
ProjectiveSpace V is at_least_3rank
by Th25; :: thesis: verum( a = 0 & b = 0 )

let a, b be Real; :: thesis: ( (a * u) + (b * v) = 0. V implies ( a = 0 & b = 0 ) )

assume (a * u) + (b * v) = 0. V ; :: thesis: ( a = 0 & b = 0 )

then 0. V = ((a * u) + (b * v)) + (0. V) by RLVECT_1:4

.= ((a * u) + (b * v)) + (0 * w1) by RLVECT_1:10 ;

hence ( a = 0 & b = 0 ) by A1; :: thesis: verum

end;assume (a * u) + (b * v) = 0. V ; :: thesis: ( a = 0 & b = 0 )

then 0. V = ((a * u) + (b * v)) + (0. V) by RLVECT_1:4

.= ((a * u) + (b * v)) + (0 * w1) by RLVECT_1:10 ;

hence ( a = 0 & b = 0 ) by A1; :: thesis: verum