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
Z0: for x being set st x in X holds
x is epsilon Ordinal and
Z1: 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 Z2: 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 Z0; :: 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 Z1, Z2, FEGT; :: thesis: verum

end;

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