let X be set ; :: thesis:
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 )

let x be set ; :: thesis:
assume x in union X ; :: thesis:
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= y1 by A2, A5, ORDINAL1:def 2;
hence x c= union X by A7; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: x in UNX ; :: thesis:
reconsider x1 = x as Ordinal by A9;
assume not x in card UNX ; :: thesis:
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:

end;