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

A4: now :: thesis:

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

per cases by A5, XXREAL_0:14;

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

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:

end;

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

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:

end;

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

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:

end;

end;

end;

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