let a, b be Ordinal; :: thesis: ( 1 in a & a in b implies a *^ b in exp (b,a) )
assume A1: ( 1 in a & a in b ) ; :: thesis: a *^ b in exp (b,a)
then A3: exp (b,2) c= exp (b,a) by Lm2, ORDINAL1:21, ORDINAL4:27;
a *^ b in b *^ b by A1, ORDINAL2:40;
then a *^ b in exp (b,2) by Th4;
hence a *^ b in exp (b,a) by A3; :: thesis: verum