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

per cases ( z = -infty or z in REAL ) by A3, XXREAL_0:14;

suppose z = -infty ; :: thesis: x / z < y / z

hence x / z < y / z by A2; :: thesis: verum

end;

suppose z in REAL ; :: thesis: x / z < y / z

then reconsider z = z as Real ;
z " > 0 by A2;
hence x / z < y / z by A1, Th72; :: thesis: verum

end;

end;