let e be epsilon Ordinal; :: thesis: omega in e
A1: exp (omega,e) = e by Def5;
A2: ( exp (omega,0) = 1 & exp (omega,1) = omega & 1 in omega ) by ORDINAL2:43, ORDINAL2:46;
then A3: ( e <> 0 & e <> 1 & succ 0 = 1 & succ 1 = 2 ) by Def5;
then 0 in e by ORDINAL3:8;
then 1 c= e by A3, ORDINAL1:21;
then 1 c< e by A3;
then 1 in e by ORDINAL1:11;
hence omega in e by A1, A2, ORDINAL4:24; :: thesis: verum