A1: A is finite ;
defpred S1[ set ] means ex B being set st
( B = A & bool B is finite );
consider G being set such that
A2: for x being set holds
( x in G iff ( x in bool A & S1[x] ) ) from XBOOLE_0:sch 1();
 defpred S2[ set ] means A in G;
{} c= A by XBOOLE_1:2;
then A3: S2[ {} ] by A2, ZFMISC_1:1;
A4: for x, B being set st x in A & B c= A & S2[B] holds
S2[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in A & B c= A & S2[B] implies S2[B \/ {x}] )
assume that
A5: x in A and
B c= A and
A6: B in G ; :: thesis: S2[B \/ {x}]
A7: now
assume x in B ; :: thesis: S2[B \/ {x}]
then {x} c= B by ZFMISC_1:37;
hence S2[B \/ {x}] by A6, XBOOLE_1:12; :: thesis: verum
end;
now
assume A8: not x in B ; :: thesis: S2[B \/ {x}]
defpred S3[ set , set ] means ex Y being set st
( Y = A & c2 = Y \/ {x} );
A9: for y, y1, y2 being set st y in bool B & S3[y,y1] & S3[y,y2] holds
y1 = y2 ;
A10: for y being set st y in bool B holds
ex z being set st S3[y,z]
proof
let y be set ; :: thesis: ( y in bool B implies ex z being set st S3[y,z] )
assume y in bool B ; :: thesis: ex z being set st S3[y,z]
ex Y being set st
( Y = y & y \/ {x} = Y \/ {x} ) ;
hence ex z being set st S3[y,z] ; :: thesis: verum
end;
consider f being Function such that
A11: dom f = bool B and
A12: for y being set st y in bool B holds
S3[y,f . y] from FUNCT_1:sch 2(A9, A10);
A13: ex A being set st
( B = A & bool A is finite ) by A2, A6;
for y being set holds
( y in rng f iff y in (bool (B \/ {x})) \ (bool B) )
proof
let y be set ; :: thesis: ( y in rng f iff y in (bool (B \/ {x})) \ (bool B) )
thus ( y in rng f implies y in (bool (B \/ {x})) \ (bool B) ) :: thesis: ( y in (bool (B \/ {x})) \ (bool B) implies y in rng f )
proof
assume y in rng f ; :: thesis: y in (bool (B \/ {x})) \ (bool B)
then consider x1 being set such that
A15: x1 in dom f and
A16: f . x1 = y by FUNCT_1:def 5;
consider X1 being set such that
A17: ( X1 = x1 & f . x1 = X1 \/ {x} ) by A11, A12, A15;
A18: X1 \/ {x} c= B \/ {x} by A11, A15, A17, XBOOLE_1:13;
x in {x} by TARSKI:def 1;
then ( x in y & not x in B ) by A8, A16, A17, XBOOLE_0:def 3;
then not y in bool B ;
hence y in (bool (B \/ {x})) \ (bool B) by A16, A17, A18, XBOOLE_0:def 5; :: thesis: verum
end;
assume A19: y in (bool (B \/ {x})) \ (bool B) ; :: thesis: y in rng f
set Z = y \ {x};
A20: now
assume A21: not x in y ; :: thesis: contradiction
y c= B
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in y or z in B )
assume z in y ; :: thesis: z in B
then ( z in B \/ {x} & not z in {x} ) by A19, A21, TARSKI:def 1;
hence z in B by XBOOLE_0:def 3; :: thesis: verum
end;
hence contradiction by A19, XBOOLE_0:def 5; :: thesis: verum
end;
A22: y \ {x} c= B by A19, XBOOLE_1:43;
then consider X being set such that
A23: X = y \ {x} and
A24: f . (y \ {x}) = X \/ {x} by A12;
X \/ {x} = y \/ {x} by A23, XBOOLE_1:39
.= y by A20, ZFMISC_1:46 ;
hence y in rng f by A11, A22, A24, FUNCT_1:def 5; :: thesis: verum
end;
then rng f = (bool (B \/ {x})) \ (bool B) by TARSKI:2;
then A25: f .: (bool B) = (bool (B \/ {x})) \ (bool B) by A11, RELAT_1:146;
A26: bool B c= bool (B \/ {x}) by XBOOLE_1:7, ZFMISC_1:79;
B27: ((bool (B \/ {x})) \ (bool B)) \/ (bool B) = (bool (B \/ {x})) \/ (bool B) by XBOOLE_1:39
.= bool (B \/ {x}) by A26, XBOOLE_1:12 ;
{x} c= A by A5, ZFMISC_1:37;
then ( B in bool A & {x} in bool A ) by A2, A6;
then B \/ {x} c= A by XBOOLE_1:8;
hence S2[B \/ {x}] by A2, B27, A13, A25; :: thesis: verum
end;
hence S2[B \/ {x}] by A7; :: thesis: verum
end;
S2[A] from FINSET_1:sch 2(A1, A3, A4);
 then ex X being set st
( X = A & bool X is finite ) by A2;
hence bool A is finite ; :: thesis: verum