theorem :: ORDINAL5:19

for a being Ordinal holds a |^|^ 3 = exp (a,(exp (a,a)))