:: deftheorem defines are_lindependent2 EUCLIDLP:def 2 :
for n being Nat
for x1, x2 being Element of REAL n holds
( x1,x2 are_lindependent2 iff for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds
( a1 = 0 & a2 = 0 ) );