theorem FPC: :: COMPLEX3:74

for a, b, c being positive Real holds (a + b) * (a + c) > a * ((a + b) + c)