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

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

end;

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

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

end;

end;

end;

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