let X be set ; :: thesis: ( ( for a being set st a in X holds
a is Ordinal ) implies union X is ordinal )
assume A1: for a being set st a in X holds
a is Ordinal ; :: thesis: union X is ordinal
thus union X is epsilon-transitive :: according to ORDINAL1:def 4 :: thesis: union X is epsilon-connected

proof

let x be set ; :: according to ORDINAL1:def 2 :: thesis: ( x in union X implies x c= union X )
assume x in union X ; :: thesis: x c= union X
then consider Y being set such that
A2: ( x in Y & Y in X ) by TARSKI:def 4;
Y is Ordinal by A1, A2;
then A3: x c= Y by A2, Def2;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in union X )
assume a in x ; :: thesis: a in union X
hence a in union X by A2, A3, TARSKI:def 4; :: thesis: verum

end;

let x be set ; :: according to ORDINAL1:def 3 :: thesis: for y being set st x in union X & y in union X & not x in y & not x = y holds
y in x
let y be set ; :: thesis: ( x in union X & y in union X & not x in y & not x = y implies y in x )
assume A4: ( x in union X & y in union X ) ; :: thesis: ( x in y or x = y or y in x )
then consider Y being set such that
A5: ( x in Y & Y in X ) by TARSKI:def 4;
consider Z being set such that
A6: ( y in Z & Z in X ) by A4, TARSKI:def 4;
( Y is Ordinal & Z is Ordinal ) by A1, A5, A6;
then ( x is Ordinal & y is Ordinal ) by A5, A6, Th23;
hence ( x in y or x = y or y in x ) by Th24; :: thesis: verum