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 )
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
; ( 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; for b being set st b in F2() & P1[b] & b c= x holds
b = x
let b be set ; ( b in F2() & P1[b] & b c= x implies b = x )
assume that
A9:
( b in F2() & P1[b] )
and
A10:
b c= x
; 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; verum