let a be positive Real; :: thesis: for b being positive heavy Real holds a / [\b/] >= a / b
let b be positive heavy Real; :: thesis: a / [\b/] >= a / b
[\b/] <= b by INT_1:def 6;
hence a / [\b/] >= a / b by XREAL_1:118; :: thesis: verum