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

now

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

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

now

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

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

( -infty <= x & y <= +infty ) by XXREAL_0:4, XXREAL_0:5;
then A6: ( -infty < x & y < +infty ) by A4, A5, XXREAL_0:1;
then reconsider a = x as Real by A1, XXREAL_0:14;
reconsider b = y as Real by A1, A6, XXREAL_0:14;
reconsider c = z as Real by A2, A3, XXREAL_0:14;
( x / z = a / c & y / z = b / c ) by A2, Th32;
hence x / z <= y / z by A1, A2, XREAL_1:74; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

then x / z = -infty by A2, A3, Def2;
hence x / z <= y / z by XXREAL_0:5; :: thesis: verum

end;

end;

end;

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