let V be non trivial RealLinearSpace; :: thesis: ( ex u, v being Element of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) implies ProjectiveSpace V is at_least_3rank )

given u, v being Element of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; :: thesis:
A2: not are_Prop u,v by ;
let p be Element of (); :: according to ANPROJ_2:def 10 :: thesis: for q being Element of () ex r being Element of () st
( p <> r & q <> r & p,q,r are_collinear )

let q be Element of (); :: thesis: ex r being Element of () st
( p <> r & q <> r & p,q,r are_collinear )

consider y being Element of V such that
A3: ( not y is zero & p = Dir y ) by ANPROJ_1:26;
consider w being Element of V such that
A4: ( not w is zero & q = Dir w ) by ANPROJ_1:26;
( not u is zero & not v is zero ) by ;
then consider z being Element of V such that
A5: not z is zero and
A6: y,w,z are_LinDep and
A7: not are_Prop y,z and
A8: not are_Prop w,z by ;
reconsider r = Dir z as Element of () by ;
take r ; :: thesis: ( p <> r & q <> r & p,q,r are_collinear )
thus p <> r by ; :: thesis: ( q <> r & p,q,r are_collinear )
thus q <> r by ; :: thesis: p,q,r are_collinear
thus p,q,r are_collinear by A3, A4, A5, A6, Th23; :: thesis: verum