:: deftheorem Def1 defines // EUCLIDLP:def 1 :
for n being Nat
for x1, x2 being Element of REAL n holds
( x1 // x2 iff ( x1 <> 0* n & x2 <> 0* n & ex r being Real st x1 = r * x2 ) );