let e be epsilon Ordinal; :: thesis: omega in e
A0: exp omega ,e = e by EPSILON;
A1: ( exp omega ,0 = 1 & exp omega ,1 = omega & 1 in omega ) by ORDINAL2:60, ORDINAL2:63;
then A2: ( e <> 0 & e <> 1 & succ 0 = 1 & succ 1 = 2 ) by A0;
then 0 in e by ORDINAL3:10;
then 1 c= e by A2, ORDINAL1:33;
then 1 c< e by A2, XBOOLE_0:def 8;
then 1 in e by ORDINAL1:21;
hence omega in e by A0, A1, ORDINAL4:24; :: thesis: verum