let x, y, z be ext-real number ; :: thesis: ( x < y & 0 < z & z <> +infty implies x / z < y / z )
assume that
A2: x < y and
A3: 0 < z and
pc: z <> +infty ; :: thesis: x / z < y / z

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

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

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

end;

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

then reconsider z = z as real number ;
z " > 0 by A3;
hence x / z < y / z by A2, Th67; :: thesis: verum

end;

end;