let X be set ; :: thesis: ( ( for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ) implies union X is Cardinal )
assume A1: for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ; :: thesis: union X is Cardinal
for x being set st x in union X holds
( x is Ordinal & x c= union X )

proof

let x be set ; :: thesis: ( x in union X implies ( x is Ordinal & x c= union X ) )
assume x in union X ; :: thesis: ( x is Ordinal & x c= union X )
then consider Y being set such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
consider y being set such that
A4: y in X and
A5: Y c= y and
A6: y is Cardinal by A1, A3;
reconsider y1 = y as Cardinal by A6;
A7: y1 c= union X by A4, ZFMISC_1:74;
x in y1 by A2, A5;
hence x is Ordinal ; :: thesis: x c= union X
x c= y1 by A2, A5, ORDINAL1:def 2;
hence x c= union X by A7; :: thesis: verum

end;

then reconsider UNX = union X as epsilon-transitive epsilon-connected set by ORDINAL1:19;
A8: UNX c= card UNX

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UNX or x in card UNX )
assume A9: x in UNX ; :: thesis: x in card UNX
reconsider x1 = x as Ordinal by A9;
assume not x in card UNX ; :: thesis: contradiction
then card UNX c= x1 by ORDINAL1:16;
then card UNX in UNX by A9, ORDINAL1:12;
then consider Y being set such that
A10: card UNX in Y and
A11: Y in X by TARSKI:def 4;
consider y being set such that
A12: y in X and
A13: Y c= y and
A14: y is Cardinal by A1, A11;
reconsider y1 = y as Cardinal by A14;
card y1 c= card UNX by A12, CARD_1:11, ZFMISC_1:74;
then A15: y1 c= card UNX ;
card UNX in y1 by A10, A13;
then card UNX in card UNX by A15;
hence contradiction ; :: thesis: verum

end;

card UNX c= UNX by CARD_1:8;
hence union X is Cardinal by A8, XBOOLE_0:def 10; :: thesis: verum