let a, b be Ordinal; :: thesis: ( 1 in a & a in b implies exp (b,a) in b |^|^ a )
assume A1: ( 1 in a & a in b ) ; :: thesis: exp (b,a) in b |^|^ a
then A2: 1 in b by ORDINAL1:10;
then 0 c< b by XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in b by ORDINAL1:11;
then A3: b |^|^ 2 c= b |^|^ a by A1, Lm2, ORDINAL1:21, ORDINAL5:21;
exp (b,a) in exp (b,b) by A1, A2, ORDINAL4:24;
then exp (b,a) in b |^|^ 2 by ORDINAL5:18;
hence exp (b,a) in b |^|^ a by A3; :: thesis: verum