let a be Ordinal; :: thesis: a |^|^ 3 = exp (a,(exp (a,a)))
3 = succ 2 ;
hence a |^|^ 3 = exp (a,(a |^|^ 2)) by Th14
.= exp (a,(exp (a,a))) by Th18 ;
:: thesis: verum