theorem PI1: :: NEWTON06:2

for a, b being positive Real holds
( [\a/] * [\b/] <= [\a/] * b & [\a/] * b <= a * b )