let V be RealLinearSpace; :: thesis: ( V is up-3-dimensional implies not V is trivial )
given u, v, w1 being Element of V such that A1: for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ; :: according to ANPROJ_2:def 6 :: thesis: not V is trivial
now :: thesis: not w1 = 0. V
assume w1 = 0. V ; :: thesis: contradiction
then A2: 0. V = 1 * w1 by RLVECT_1:10;
( 0. V = 0 * u & 0. V = 0 * v ) by RLVECT_1:10;
then 0. V = (0 * u) + (0 * v) by RLVECT_1:4
.= ((0 * u) + (0 * v)) + (1 * w1) by A2, RLVECT_1:4 ;
hence contradiction by A1; :: thesis: verum
end;
hence not V is trivial ; :: thesis: verum