let b, a be ordinal number ; :: thesis: ( 1 in b implies a in exp b,(succ (b -exponent a)) )
assume Z0: 1 in b ; :: thesis: a in exp b,(succ (b -exponent a))

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

suppose A0: 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:26;
then ( succ (b -exponent a) c= b -exponent a & b -exponent a in succ (b -exponent a) ) by Z0, A0, EXP, ORDINAL1:10;
then b -exponent a in b -exponent a ;
hence contradiction ; :: thesis: verum

end;

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

then b -exponent a = 0 by EXP;
then exp b,(succ (b -exponent a)) = b by ORDINAL2:63;
hence a in exp b,(succ (b -exponent a)) by Z0, A1, Lem0, ORDINAL1:19; :: thesis: verum

end;

end;