let X be non empty set ; :: thesis: ( ( for x being set st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ) implies union X is epsilon Ordinal )
assume Z0: for x being set st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ; :: thesis: union X is epsilon Ordinal
then for x being set st x in X holds
x is Ordinal ;
then reconsider a = union X as Ordinal by ORDINAL1:35;

now

let b be ordinal number ; :: thesis: ( b in a implies succ b in a )
assume b in a ; :: thesis: succ b in a
then consider x being set such that
B1: ( b in x & x in X ) by TARSKI:def 4;
reconsider x = x as epsilon Ordinal by B1, Z0;
succ b in x by B1, ORDINAL1:41;
hence succ b in a by B1, TARSKI:def 4; :: thesis: verum

end;

then Z1: a is limit_ordinal by ORDINAL1:41;
set z = the Element of X;
ex e being epsilon Ordinal st
( the Element of X in e & e in X ) by Z0;
then Z2: a <> {} by TARSKI:def 4;
a is epsilon

proof

thus exp omega ,a c= a :: according to XBOOLE_0:def 10,ORDINAL5:def 5 :: thesis: a c= exp omega ,a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in exp omega ,a or x in a )
assume x in exp omega ,a ; :: thesis: x in a
then consider b being ordinal number such that
Z3: ( b in a & x in exp omega ,b ) by Z1, Z2, Th005;
consider y being set such that
Z4: ( b in y & y in X ) by Z3, TARSKI:def 4;
reconsider y = y as epsilon Ordinal by Z0, Z4;
exp omega ,b in exp omega ,y by Z4, ORDINAL4:24;
then exp omega ,b in y by EPSILON;
then x in y by Z3, ORDINAL1:19;
hence x in a by Z4, TARSKI:def 4; :: thesis: verum

end;

thus a c= exp omega ,a by ORDINAL4:32; :: thesis: verum

end;

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