now

defpred S₁[ set ] means ex B being set st
( B = $1 & P₁[B] );
assume F₂() <> {} ; :: thesis: P₁[F₂()]
consider G being set such that
A4: for x being set holds
( x in G iff ( x in bool F₂() & S₁[x] ) ) from XBOOLE_0:sch 1();
G c= bool F₂()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in bool F₂() )
assume x in G ; :: thesis: x in bool F₂()
hence x in bool F₂() by A4; :: thesis: verum

end;

then reconsider GA = G as Subset-Family of F₂() ;
{} c= F₂() by XBOOLE_1:2;
then GA <> {} by A2, A4;
then consider B being set such that
A5: B in GA and
A6: for X being set st X in GA & B c= X holds
B = X by A1, FINSET_1:18;
A7: ex A being set st
( A = B & P₁[A] ) by A4, A5;

now

consider x being Element of F₂() \ B;
assume B <> F₂() ; :: thesis: contradiction
then not F₂() c= B by A5, XBOOLE_0:def 10;
then A8: F₂() \ B <> {} by XBOOLE_1:37;
then not x in B by XBOOLE_0:def 5;
then not {x} c= B by ZFMISC_1:37;
then A9: B \/ {x} <> B by XBOOLE_1:7;
A10: x in F₂() by A8, XBOOLE_0:def 5;
then {x} c= F₂() by ZFMISC_1:37;
then A11: B \/ {x} c= F₂() by A5, XBOOLE_1:8;
B is Subset of F₁() by A5, XBOOLE_1:1;
then P₁[B \/ {x}] by A3, A5, A7, A10;
then B \/ {x} in GA by A4, A11;
hence contradiction by A6, A9, XBOOLE_1:7; :: thesis: verum

end;

hence P₁[F₂()] by A7; :: thesis: verum

end;

hence P₁[F₂()] by A2; :: thesis: verum