:: deftheorem defines are_LinDep ANPROJ_1:def 2 :
for V being RealLinearSpace
for u, v, w being Element of V holds
( u,v,w are_LinDep iff ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) );