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:
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 ;
x in y1 by A2, A5;
hence x is Ordinal ; :: thesis: x c= union X
x c= y1 by ;
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 ;
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 ;
reconsider y1 = y as Cardinal by A14;
card y1 c= card UNX by ;
then A15: y1 c= card UNX ;
card UNX in y1 by ;
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 ; :: thesis: verum