let a be ordinal number ; :: thesis: a in exp omega ,(succ (omega -exponent a))

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

suppose A0: 0 in a ; :: thesis: a in exp omega ,(succ (omega -exponent a))

assume not a in exp omega ,(succ (omega -exponent a)) ; :: thesis: contradiction
then exp omega ,(succ (omega -exponent a)) c= a by ORDINAL1:26;
then ( succ (omega -exponent a) c= omega -exponent a & omega -exponent a in succ (omega -exponent a) ) by A0, EXP, ORDINAL1:10;
then omega -exponent a in omega -exponent a ;
hence contradiction ; :: thesis: verum

end;

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

then omega -exponent a = 0 by EXP;
then exp omega ,(succ (omega -exponent a)) = omega by ORDINAL2:63;
hence a in exp omega ,(succ (omega -exponent a)) by A1; :: thesis: verum

end;

end;