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