theorem Th93: :: NUMBER17:93

for a, b, c, d being positive Real holds (GMean <*a,b,c,d*>) |^ 4 = ((a * b) * c) * d