let x, y, k be Real; :: thesis: ( k <= 0 implies ( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) ) )
assume A1: k <= 0 ; :: thesis: ( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) )
hereby :: thesis: k * (max (x,y)) = min ((k * x),(k * y))
per cases ( max (x,y) = x or max (x,y) = y ) by XXREAL_0:16;
suppose max (x,y) = x ; :: thesis: k * (min (x,y)) = max ((k * x),(k * y))
then A2: y <= x by XXREAL_0:def 10;
then max ((k * x),(k * y)) = k * y by ;
hence k * (min (x,y)) = max ((k * x),(k * y)) by ; :: thesis: verum
end;
suppose max (x,y) = y ; :: thesis: k * (min (x,y)) = max ((k * x),(k * y))
then A3: x <= y by XXREAL_0:def 10;
then max ((k * x),(k * y)) = k * x by ;
hence k * (min (x,y)) = max ((k * x),(k * y)) by ; :: thesis: verum
end;
end;
end;
per cases ( min (x,y) = x or min (x,y) = y ) by XXREAL_0:15;
suppose min (x,y) = x ; :: thesis: k * (max (x,y)) = min ((k * x),(k * y))
then A4: x <= y by XXREAL_0:def 9;
then min ((k * x),(k * y)) = k * y by ;
hence k * (max (x,y)) = min ((k * x),(k * y)) by ; :: thesis: verum
end;
suppose min (x,y) = y ; :: thesis: k * (max (x,y)) = min ((k * x),(k * y))
then A5: y <= x by XXREAL_0:def 9;
then min ((k * y),(k * x)) = k * x by ;
hence k * (max (x,y)) = min ((k * x),(k * y)) by ; :: thesis: verum
end;
end;