let x, y, z be ExtReal; :: thesis: ( x < y & 0 < z & z <> +infty implies x * z < y * z )
assume that
A1: x < y and
A2: 0 < z and
A3: z <> +infty ; :: thesis: x * z < y * z

A4: now :: thesis: not x * z = y * z

A5: ( x <> +infty & y <> -infty ) by A1, XXREAL_0:3, XXREAL_0:5;
assume A6: x * z = y * z ; :: thesis: contradiction

per cases ( ( x in REAL & y in REAL ) or y = +infty or x = -infty ) by A5, XXREAL_0:14;

suppose A7: ( x in REAL & y in REAL ) ; :: thesis: contradiction

z in REAL by A2, A3, XXREAL_0:14;
then reconsider x = x, y = y, z = z as Real by A7;
x * z < y * z by A1, A2, XREAL_1:68;
hence contradiction by A6; :: thesis: verum

end;

suppose A8: y = +infty ; :: thesis: contradiction

then y * z = +infty by A2, Def5;
then ( x = +infty or x = -infty ) by A2, A3, A6, Th69;
hence contradiction by A1, A2, A6, A8; :: thesis: verum

end;

suppose A9: x = -infty ; :: thesis: contradiction

then x * z = -infty by A2, Def5;
then ( y = +infty or y = -infty ) by A2, A3, A6, Th70;
hence contradiction by A1, A2, A6, A9; :: thesis: verum

end;

end;

end;

x * z <= y * z by A1, A2, Th71;
hence x * z < y * z by A4, XXREAL_0:1; :: thesis: verum