let X be non empty set ; :: thesis:
assume that
A1: for x being object st x in X holds
x is epsilon Ordinal and
A2: for a being Ordinal st a in X holds
first_epsilon_greater_than a in X ; :: thesis:

let x be object ; :: thesis:
assume A3: x in X ; :: thesis:
hence x is epsilon Ordinal by A1; :: thesis:
reconsider a = x as Ordinal by A1, A3;
take e = first_epsilon_greater_than a; :: thesis:
thus ( x in e & e in X ) by A2, A3, Def6; :: thesis:

end;

hence union X is epsilon Ordinal by Th49; :: thesis: