let a, b be positive Real; :: thesis: [\a/] * [\b/] <= [\(a * b)/]
( [\a/] * [\b/] <= [\a/] * b & [\a/] * b <= a * b ) by PI1;
then [\a/] * [\b/] <= a * b by XXREAL_0:2;
hence [\a/] * [\b/] <= [\(a * b)/] by INT_1:54; :: thesis: verum