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