theorem Th99: :: NUMBER17:99
for a, b, c, d being positive Real st ((a * b) * c) * d >= ((((a + b) + c) + d) / 4) |^ 4 holds
( a = b & b = c & c = d )