theorem Th5: :: ACKERMAN:5

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