theorem Th32: :: EUCLIDLP:32

for n being Nat
for x1, x2 being Element of REAL n st x1 // x2 holds
ex a being Real st
( a <> 0 & x1 = a * x2 )