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