let e be Ordinal; :: thesis: ( e is epsilon implies ( not e is empty & e is limit_ordinal ) )
assume A0: e is epsilon ; :: thesis: ( not e is empty & e is limit_ordinal )
exp omega ,0 = 1 by ORDINAL2:60;
hence not e is empty by A0, EPSILON; :: thesis: e is limit_ordinal
then ( 0 in e & exp omega ,e = e ) by A0, EPSILON, ORDINAL3:10;
hence e is limit_ordinal by Th002; :: thesis: verum