defpred S₁[ object ] means ex y being object st A = {y};
consider X being set such that
A1: for x being object holds
( x in X iff ( x in bool A & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being object holds
( x in union X iff x in A )

proof

let x be object ; :: thesis: ( x in union X iff x in A )
thus ( x in union X implies x in A ) :: thesis: ( x in A implies x in union X )

proof

assume x in union X ; :: thesis: x in A
then consider B being set such that
A2: x in B and
A3: B in X by TARSKI:def 4;
B in bool A by A1, A3;
hence x in A by A2; :: thesis: verum

end;

assume x in A ; :: thesis: x in union X
then {x} c= A by ZFMISC_1:31;
then A4: {x} in X by A1;
x in {x} by TARSKI:def 1;
hence x in union X by A4, TARSKI:def 4; :: thesis: verum

end;

then A5: union X = A by TARSKI:2;
A6: for B being set st B in X holds
B is finite

proof

let B be set ; :: thesis: ( B in X implies B is finite )
assume B in X ; :: thesis: B is finite
then ex y being object st B = {y} by A1;
hence B is finite ; :: thesis: verum

end;

A7: X c= bool A by A1;
assume bool A is finite ; :: thesis: contradiction
hence contradiction by A5, A6, A7, FINSET_1:7; :: thesis: verum