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

now

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

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

then x / z = 0. by A1, A4, Def2;
hence y / z <= x / z by A1, A4, A5, Def2; :: thesis: verum

end;

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

then reconsider c = z as Real by A3, XXREAL_0:14;
( x / z = a / c & y / z = b / c ) by A3, Th32;
hence y / z <= x / z by A2, A3, XREAL_1:75; :: thesis: verum

end;

end;

end;

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