let a, b be positive Real; :: thesis: ( [\a/] * [\b/] <= [\a/] * b & [\a/] * b <= a * b )
( [\a/] <= a & [\b/] <= b ) by INT_1:def 6;
hence ( [\a/] * [\b/] <= [\a/] * b & [\a/] * b <= a * b ) by XREAL_1:64; :: thesis: verum