let x, y, z be R_eal; :: thesis: ( x < y & z < 0. & z <> -infty implies y / z < x / z )
assume that
A1: x < y and
A2: ( z < 0. & z <> -infty ) ; :: thesis: y / z < x / z
A3: ( x <> +infty & y <> -infty ) by A1, XXREAL_0:4, XXREAL_0:5;
reconsider c = z as Real by A2, XXREAL_0:14;

per cases ( y <> +infty or y = +infty ) ;

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

then reconsider b = y as Real by A3, XXREAL_0:14;
A4: y / z = b / c by A2, Th32;

now

per cases ( x <> -infty or x = -infty ) ;

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

then reconsider a = x as Real by A3, XXREAL_0:14;
x / z = a / c by A2, Th32;
hence y / z < x / z by A1, A2, A4, XREAL_1:77; :: thesis: verum

end;

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

then x / z = +infty by A2, Def2;
hence y / z < x / z by A4, XXREAL_0:9; :: thesis: verum

end;

end;

end;

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

end;

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

then A5: y / z = -infty by A2, Def2;

now

per cases ( x <> -infty or x = -infty ) ;

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

then reconsider a = x as Real by A3, XXREAL_0:14;
x / z = a / c by A2, Th32;
hence y / z < x / z by A5, XXREAL_0:12; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;