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

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

hence
not V is trivial
; :: thesis: verumassume
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;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