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_{1}, b_{2} being Element of the U1 of (ProjectiveSpace V) holds p,b_{1},b_{2} are_collinear

take q ; :: thesis: not for b_{1} being Element of the U1 of (ProjectiveSpace V) holds p,q,b_{1} 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

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

take q ; :: thesis: not for b

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