theorem MES57: :: FUZNORM1:17

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