reconsider a = F1() as finite set by A2;
defpred S1[ set ] means ( $1 c= F1() & P1[$1] );
consider X being set such that
A3: for x being set holds
( x in X iff ( x in F2() & S1[x] ) ) from XFAMILY:sch 1();
 A4: ( bool a is finite & X c= bool a )
proof
thus bool a is finite ; :: thesis: X c= bool a
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in bool a )
reconsider xx = x as set by TARSKI:1;
assume x in X ; :: thesis: x in bool a
then xx c= a by A3;
hence x in bool a ; :: thesis: verum
end;
defpred S2[ set , set ] means $1 c= $2;
A5: for x, y being set st S2[x,y] & S2[y,x] holds
x = y ;
A6: for x, y, z being set st S2[x,y] & S2[y,z] holds
S2[x,z] by XBOOLE_1:1;
reconsider X = X as finite set by A4;
A7: X <> {} by A1, A3;
consider x being set such that
A8: ( x in X & ( for y being set st y in X & y <> x holds
not S2[y,x] ) ) from CARD_2:sch 3(A7, A5, A6);
 take x ; :: thesis: ( x in F2() & P1[x] & ( for b being set st b in F2() & P1[b] & b c= x holds
b = x ) )
thus ( x in F2() & P1[x] ) by A3, A8; :: thesis: for b being set st b in F2() & P1[b] & b c= x holds
b = x
let b be set ; :: thesis: ( b in F2() & P1[b] & b c= x implies b = x )
assume that
A9: ( b in F2() & P1[b] ) and
A10: b c= x ; :: thesis: b = x
x c= a by A3, A8;
then b c= a by A10;
then b in X by A3, A9;
hence b = x by A8, A10; :: thesis: verum