theorem :: EUCLIDLP:42

for n being Nat
for x1, x2 being Element of REAL n holds
( not x1,x2 are_ldependent2 or x1 = 0* n or x2 = 0* n or x1 // x2 ) by Lm4;