let x, y, z be ext-real number ; :: 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, Th83;
( - (x * z) = x * (- z) & - (y * z) = y * (- z) ) by Th103;
hence y * z < x * z by A1, Th40; :: thesis: verum