theorem :: NUMBER17:92

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