let C, A be Ordinal; :: thesis: ( 1 in C implies exp (C,A) in exp (C,(succ A)) )
A1: 1 *^ (exp (C,A)) = exp (C,A) by ORDINAL2:56;
assume 1 in C ; :: thesis: exp (C,A) in exp (C,(succ A))
then exp (C,A) in C *^ (exp (C,A)) by A1, Th22, ORDINAL2:57;
hence exp (C,A) in exp (C,(succ A)) by ORDINAL2:61; :: thesis: verum