let X be non empty set ; :: thesis: ( ( for x being set st x in X holds
x is epsilon Ordinal ) & ( for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ) implies union X is epsilon Ordinal )
assume that
A1: for x being set st x in X holds
x is epsilon Ordinal and
A2: for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ; :: thesis: union X is epsilon Ordinal

now

let x be set ; :: 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 )
then reconsider a = x as Ordinal ;
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