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 is zero & not v is zero & not w is zero ) by A1, Th1;
A3: not u,v,w are_LinDep by A1, Th1;
reconsider p = Dir u, q = Dir v, r = Dir w as Element of (ProjectiveSpace V) by A2, ANPROJ_1:42;
take p ; :: according to COLLSP:def 6 :: thesis: not for b₁, b₂ being Element of the carrier of (ProjectiveSpace V) holds p,b₁,b₂ is_collinear
take q ; :: thesis: not for b₁ being Element of the carrier of (ProjectiveSpace V) holds p,q,b₁ is_collinear
take r ; :: thesis: not p,q,r is_collinear
assume p,q,r is_collinear ; :: thesis: contradiction
then [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) by COLLSP:def 2;
hence contradiction by A2, A3, ANPROJ_1:41; :: thesis: verum