theorem Th37: :: EUCLIDLP:37

for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 <> x2