let V be non trivial RealLinearSpace; :: thesis: ( V is up-3-dimensional implies ProjectiveSpace V is proper )
given u, v, w being Element of V such that A1: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ; :: according to ANPROJ_2:def 6 :: thesis: ProjectiveSpace V is proper
A2: not u,v,w are_LinDep by A1;
A3: not w is zero by A1, Th1;
A4: ( not u is zero & not v is zero ) by A1, Th1;
then reconsider p = Dir u, q = Dir v, r = Dir w as Element of (ProjectiveSpace V) by A3, ANPROJ_1:26;
take p ; :: according to COLLSP:def 6 :: thesis: not for b₁, b₂ being Element of the U1 of (ProjectiveSpace V) holds p,b₁,b₂ are_collinear
take q ; :: thesis: not for b₁ being Element of the U1 of (ProjectiveSpace V) holds p,q,b₁ are_collinear
take r ; :: thesis: not p,q,r are_collinear
assume p,q,r are_collinear ; :: thesis: contradiction
then [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) ;
hence contradiction by A4, A3, A2, ANPROJ_1:25; :: thesis: verum