for a, b, c being Real st 0 <= c holds
( c * (max (a,b)) = max ((c * a),(c * b)) & c * (min (a,b)) = min ((c * a),(c * b)) ) by Lm1, Lm2;