let A, C 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:39;
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:40;
hence exp (C,A) in exp (C,(succ A)) by ORDINAL2:44; :: thesis: verum