assume A28: bool A is finite ; :: thesis: contradiction
defpred S₁[ set ] means ex y being set st A = {y};
consider X being set such that
A29: for x being set holds
( x in X iff ( x in bool A & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being set holds
( x in union X iff x in A )

proof

let x be set ; :: 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
A30: x in B and
A31: B in X by TARSKI:def 4;
B in bool A by A29, A31;
hence x in A by A30; :: thesis: verum

end;

assume x in A ; :: thesis: x in union X
then {x} c= A by ZFMISC_1:37;
then A32: {x} in X by A29;
x in {x} by TARSKI:def 1;
hence x in union X by A32, TARSKI:def 4; :: thesis: verum

end;

then A33: union X = A by TARSKI:2;
A34: 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 set st B = {y} by A29;
hence B is finite ; :: thesis: verum

end;

X c= bool A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in bool A )
assume x in X ; :: thesis: x in bool A
hence x in bool A by A29; :: thesis: verum

end;

then X is finite by A28;
hence contradiction by A33, A34, FINSET_1:25; :: thesis: verum