let e be Ordinal; :: thesis: ( e is epsilon implies ( not e is empty & e is limit_ordinal ) )
assume A1: e is epsilon ; :: thesis: ( not e is empty & e is limit_ordinal )
exp (omega,0) = 1 by ORDINAL2:43;
hence not e is empty by A1; :: thesis: e is limit_ordinal
then ( 0 in e & exp (omega,e) = e ) by A1, ORDINAL3:8;
hence e is limit_ordinal by Th9; :: thesis: verum