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: ProjectiveSpace V is at_least_3rank

A2: not are_Prop u,v by A1, Lm1;

let p be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 10 :: thesis: for q being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st

( p <> r & q <> r & p,q,r are_collinear )

let q be Element of (ProjectiveSpace V); :: thesis: ex r being Element of (ProjectiveSpace V) 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 A1, Lm1;

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 A2, ANPROJ_1:16;

reconsider r = Dir z as Element of (ProjectiveSpace V) by A5, ANPROJ_1:26;

take r ; :: thesis: ( p <> r & q <> r & p,q,r are_collinear )

thus p <> r by A3, A5, A7, ANPROJ_1:22; :: thesis: ( q <> r & p,q,r are_collinear )

thus q <> r by A4, A5, A8, ANPROJ_1:22; :: thesis: p,q,r are_collinear

thus p,q,r are_collinear by A3, A4, A5, A6, Th23; :: thesis: verum

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: ProjectiveSpace V is at_least_3rank

A2: not are_Prop u,v by A1, Lm1;

let p be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 10 :: thesis: for q being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st

( p <> r & q <> r & p,q,r are_collinear )

let q be Element of (ProjectiveSpace V); :: thesis: ex r being Element of (ProjectiveSpace V) 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 A1, Lm1;

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 A2, ANPROJ_1:16;

reconsider r = Dir z as Element of (ProjectiveSpace V) by A5, ANPROJ_1:26;

take r ; :: thesis: ( p <> r & q <> r & p,q,r are_collinear )

thus p <> r by A3, A5, A7, ANPROJ_1:22; :: thesis: ( q <> r & p,q,r are_collinear )

thus q <> r by A4, A5, A8, ANPROJ_1:22; :: thesis: p,q,r are_collinear

thus p,q,r are_collinear by A3, A4, A5, A6, Th23; :: thesis: verum