:: deftheorem defines are_lindependent2 EUCLID_3:def 10 :
for n being Element of NAT
for q1, q2 being Point of (TOP-REAL n) holds
( q1,q2 are_lindependent2 iff for a1, a2 being Real st (a1 * q1) + (a2 * q2) = 0. (TOP-REAL n) holds
( a1 = 0 & a2 = 0 ) );