let x, y, k be R_eal; :: 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 k * x <= k * y by A1, XXREAL_3:113;
then max (k * x),(k * y) = k * y by XXREAL_0:def 10;
hence k * (min x,y) = max (k * x),(k * y) by A2, XXREAL_0:def 9; :: 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 k * y <= k * x by A1, XXREAL_3:113;
then max (k * x),(k * y) = k * x by XXREAL_0:def 10;
hence k * (min x,y) = max (k * x),(k * y) by A3, XXREAL_0:def 9; :: 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 k * y <= k * x by A1, XXREAL_3:113;
then min (k * x),(k * y) = k * y by XXREAL_0:def 9;
hence k * (max x,y) = min (k * x),(k * y) by A4, XXREAL_0:def 10; :: 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 k * x <= k * y by A1, XXREAL_3:113;
then min (k * y),(k * x) = k * x by XXREAL_0:def 9;
hence k * (max x,y) = min (k * x),(k * y) by A5, XXREAL_0:def 10; :: thesis: verum

end;

end;