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