let a, b, c be Ordinal; :: 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:21;
then A2: exp (c,(succ (c -exponent b))) c= exp (c,(c -exponent a)) by A1, ORDINAL4:27;
A3: 0 in a by A1, Def10;
b in exp (c,(succ (c -exponent b))) by A1, Th57;
then ( b in exp (c,(c -exponent a)) & exp (c,(c -exponent a)) c= a ) by A1, A2, A3, Def10;
hence b in a ; :: thesis: verum