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
A14: x1 in dom f and
A15: f . x1 = y by FUNCT_1:def 5;
consider X1 being set such that
A16: X1 = x1 and
A17: f . x1 = X1 \/ {x} by A11, A12, A14;
A18: X1 \/ {x} c= B \/ {x} by A11, A14, A16, XBOOLE_1:13;
x in {x} by TARSKI:def 1;
then x in y by A15, A17, XBOOLE_0:def 3;
then not y in bool B by A8;
hence y in (bool (B \/ {x})) \ (bool B) by A15, 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 A22: z in y ; :: thesis: z in B
then not z in {x} by A21, TARSKI:def 1;
hence z in B by A19, A22, XBOOLE_0:def 3; :: thesis: verum
end;
hence contradiction by A19, XBOOLE_0:def 5; :: thesis: verum
end;
A23: y \ {x} c= B by A19, XBOOLE_1:43;
then consider X being set such that
A24: X = y \ {x} and
A25: f . (y \ {x}) = X \/ {x} by A12;
X \/ {x} = y \/ {x} by A24, XBOOLE_1:39
.= y by A20, ZFMISC_1:46 ;
hence y in rng f by A11, A23, A25, FUNCT_1:def 5; :: thesis: verum
end;
then rng f = (bool (B \/ {x})) \ (bool B) by TARSKI:2;
then A26: f .: (bool B) = (bool (B \/ {x})) \ (bool B) by A11, RELAT_1:146;
A27: bool B c= bool (B \/ {x}) by XBOOLE_1:7, ZFMISC_1:79;
A28: ((bool (B \/ {x})) \ (bool B)) \/ (bool B) = (bool (B \/ {x})) \/ (bool B) by XBOOLE_1:39
.= bool (B \/ {x}) by A27, XBOOLE_1:12 ;
A29: {x} c= A by A5, ZFMISC_1:37;
B in bool A by A2, A6;
then B \/ {x} c= A by A29, XBOOLE_1:8;
hence S2[B \/ {x}] by A2, A13, A26, A28; :: 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