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