let x, y, z be ext-real number ; :: thesis: ( x < y & z < 0 & z <> -infty implies y * z < x * z )
assume that
A1: x < y and
A2: z < 0 and
A3: z <> -infty ; :: thesis: y * z < x * z
B: - (x * z) = x * (- z) by Th8o;
C: - (y * z) = y * (- z) by Th8o;
x * (- z) < y * (- z) by A1, Th67, Tx4A, A3, ThM3, A2;
hence y * z < x * z by Th38, B, C; :: thesis: verum