theorem :: EUCLIDLP:41

for n being Nat
for x1, x2 being Element of REAL n st x1 // x2 holds
( x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n ) by Lm3;