theorem :: EUCLIDLP:46

for n being Nat
for x1, x2 being Element of REAL n st x1 // x2 holds
not x1 _|_ x2