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;