theorem Th45: :: EUCLIDLP:45

for n being Nat
for x, y being Element of REAL n st x _|_ y holds
x,y are_lindependent2