theorem Th4: :: ACKERMAN:4

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