:: deftheorem Def6 defines first_epsilon_greater_than ORDINAL5:def 6 :
for a being Ordinal
for b₂ being epsilon Ordinal holds
( b₂ = first_epsilon_greater_than a iff ( a in b₂ & ( for b being epsilon Ordinal st a in b holds
b₂ c= b ) ) );