let a, b be Ordinal; :: thesis: ( 1 in b implies a in exp (b,(succ (b -exponent a))) )
assume A1: 1 in b ; :: thesis: a in exp (b,(succ (b -exponent a)))

per cases ( 0 in a or a = 0 ) by ORDINAL3:8;

suppose A2: 0 in a ; :: thesis: a in exp (b,(succ (b -exponent a)))

assume not a in exp (b,(succ (b -exponent a))) ; :: thesis: contradiction
then exp (b,(succ (b -exponent a))) c= a by ORDINAL1:16;
then ( succ (b -exponent a) c= b -exponent a & b -exponent a in succ (b -exponent a) ) by A1, A2, Def10, ORDINAL1:6;
then b -exponent a in b -exponent a ;
hence contradiction ; :: thesis: verum

end;

suppose A3: a = 0 ; :: thesis: a in exp (b,(succ (b -exponent a)))

then b -exponent a = 0 by Def10;
then exp (b,(succ (b -exponent a))) = b by ORDINAL2:46;
hence a in exp (b,(succ (b -exponent a))) by A1, A3, Lm1, ORDINAL1:10; :: thesis: verum

end;

end;