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