theorem :: EUCLIDLP:38

for n being Nat
for x1, x2, x3 being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 holds
x2 <> x3 by Th37;