theorem Th4: :: HOLDER_1:4

for a, b, p, q being Real st 1 < p & (1 / p) + (1 / q) = 1 & 0 < a & 0 < b holds
( a * b <= ((a #R p) / p) + ((b #R q) / q) & ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q ) & ( a #R p = b #R q implies a * b = ((a #R p) / p) + ((b #R q) / q) ) )