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

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

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

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

end;

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

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

end;

end;