let x, y, z be ExtReal; :: thesis: ( x <= y & z <= 0 implies y * z <= x * z )
assume ( x <= y & z <= 0 ) ; :: thesis: y * z <= x * z
then A1: x * (- z) <= y * (- z) by Th71;
( - (x * z) = x * (- z) & - (y * z) = y * (- z) ) by Th92;
hence y * z <= x * z by A1, Th38; :: thesis: verum