let X be set ; :: thesis: ( ( for a being object st a in X holds
a is Ordinal ) implies ex A being Ordinal st X c= A )
assume A1: for a being object st a in X holds
a is Ordinal ; :: thesis: ex A being Ordinal st X c= A
then A2: ( union X is epsilon-transitive & union X is epsilon-connected ) by Th19;
then reconsider A = succ (union X) as Ordinal ;
take A ; :: thesis: X c= A
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in A )
assume A3: a in X ; :: thesis: a in A
then reconsider B = a as Ordinal by A1;
for b being object st b in B holds
b in union X by A3, TARSKI:def 4;
then B c= union X ;
hence a in A by A2, Th18; :: thesis: verum