theorem Th6: :: MESFUNC5:6
for x, y, k being ExtReal st 0 <= k holds
( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) )