for x, y being Element of [:REAL,REAL:] holds Eukl_dist2 . (x,y) = Eukl_dist2 . (y,x)