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