let a, b be Ordinal; ( 1 in a & a in b implies exp (b,a) in b |^|^ a )
assume A1:
( 1 in a & a in b )
; 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; verum