let c, b, a be ordinal number ; :: thesis: ( 1 in c & c -exponent b in c -exponent a implies b in a )
assume A1: ( 1 in c & c -exponent b in c -exponent a ) ; :: thesis: b in a
then succ (c -exponent b) c= c -exponent a by ORDINAL1:33;
then A3: exp (c,(succ (c -exponent b))) c= exp (c,(c -exponent a)) by A1, ORDINAL4:27;
A4: 0 in a by A1, EXP;
b in exp (c,(succ (c -exponent b))) by A1, Th41;
then ( b in exp (c,(c -exponent a)) & exp (c,(c -exponent a)) c= a ) by A1, A3, A4, EXP;
hence b in a ; :: thesis: verum