let x, y, z be ext-real number ; :: 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
X: x * z <= y * z by A1, A2, Th65;

now

assume Z: x * z = y * z ; :: thesis: contradiction
K: x <> +infty by A1, XXREAL_0:3;
L: y <> -infty by A1, XXREAL_0:5;

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

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

z in REAL by A3, A2, XXREAL_0:14;
then reconsider x = x, y = y, z = z as real number by S;
x * z < y * z by A1, A2, XREAL_1:70;
hence contradiction by Z; :: thesis: verum

end;

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

then y * z = +infty by A2, Def4;
then ( x = +infty or x = -infty ) by Th61, A3, Z, A2;
hence contradiction by A1, U, A2, Z; :: thesis: verum

end;

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

then x * z = -infty by A2, Def4;
then ( y = +infty or y = -infty ) by Th62, A3, Z, A2;
hence contradiction by A1, U, A2, Z; :: thesis: verum

end;

end;

end;

hence x * z < y * z by X, XXREAL_0:1; :: thesis: verum