let X be set ; :: thesis: ( ( for a being set st a in X holds
a is cardinal number ) implies union X is cardinal number )
assume A1: for a being set st a in X holds
a is cardinal number ; :: thesis: union X is cardinal number
now :: thesis: for a being set st a in X holds
ex b being set st
( b in X & a c= b & b is cardinal set )
let a be set ; :: thesis: ( a in X implies ex b being set st
( b in X & a c= b & b is cardinal set ) )
assume A2: a in X ; :: thesis: ex b being set st
( b in X & a c= b & b is cardinal set )
then a is cardinal number by A1;
hence ex b being set st
( b in X & a c= b & b is cardinal set ) by A2; :: thesis: verum
end;
hence union X is cardinal number by CARD_LAR:32; :: thesis: verum