for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega