:: deftheorem Def5 defines epsilon ORDINAL5:def 5 :
for a being Ordinal holds
( a is epsilon iff exp (omega,a) = a );