:: deftheorem defines _|_ EUCLIDLP:def 3 :
for n being Nat
for x1, x2 being Element of REAL n holds
( x1 _|_ x2 iff ( x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal ) );