theorem Th3: :: ACKERMAN:3

for m being Nat holds m |^|^ 3 = m |^ (m |^ m) by Lm5;