let X be non empty set ; :: thesis: ( ( 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 ) implies union X is epsilon Ordinal )
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: union X is epsilon Ordinal

now :: thesis: for x being object st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) )

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

end;

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