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

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

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

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

end;

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

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

end;

end;