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

now :: thesis: for a, b being Real st (a * u) + (b * v) = 0. V holds
( 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;

hence ProjectiveSpace V is at_least_3rank by Th25; :: thesis: verum