for X being non empty set st ( for x being object st x in X holds
x is epsilon Ordinal ) & ( for a being Ordinal st a in X holds
first_epsilon_greater_than a in X ) holds
union X is epsilon Ordinal