let a, b be positive Real; :: thesis: [\a/] / b <= a / b
[\a/] <= a by INT_1:def 6;
hence [\a/] / b <= a / b by XREAL_1:72; :: thesis: verum