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 A2: x in union X ; :: thesis: ( x is Ordinal & x c= union X )
consider Y being set such that
A3: x in Y and
A4: Y in X by A2, TARSKI:def 4;
consider y being set such that
A5: y in X and
A6: Y c= y and
A7: y is Cardinal by A1, A4;
reconsider y1 = y as Cardinal by A7;
x in y1 by A3, A6;
hence x is Ordinal ; :: thesis: x c= union X
A8: x c= y1 by A3, A6, ORDINAL1:def 2;
y1 c= union X by A5, ZFMISC_1:92;
hence x c= union X by A8, XBOOLE_1:1; :: thesis: verum

end;

then reconsider UNX = union X as Ordinal by ORDINAL1:31;
A9: card UNX c= UNX by CARD_1:24;
UNX c= card UNX

proof

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

end;

hence union X is Cardinal by A9, XBOOLE_0:def 10; :: thesis: verum