:: deftheorem Def6 defines up-3-dimensional ANPROJ_2:def 6 :
for IT being RealLinearSpace holds
( IT is up-3-dimensional iff ex u, v, w1 being Element of IT st
for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. IT holds
( a = 0 & b = 0 & c = 0 ) );