for x, y, k being R_eal st k <= 0 holds
( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) )