now

assume F₂() <> {} ; :: thesis: P₁[F₂()]
defpred S₁[ set ] means ex B being set st
( B = $1 & P₁[B] );
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₂() & P₁[ {} ] ) by A2, XBOOLE_1:2;
then GA <> {} by A4;
then consider B being set such that
A5: ( B in GA & ( for X being set st X in GA & B c= X holds
B = X ) ) by A1, FINSET_1:18;
A6: ( B in bool F₂() & 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 A7: F₂() \ B <> {} by XBOOLE_1:37;
then A8: x in F₂() by XBOOLE_0:def 5;
B is Subset of F₁() by A5, XBOOLE_1:1;
then A9: P₁[B \/ {x}] by A3, A6, A8;
{x} c= F₂() by A8, ZFMISC_1:37;
then B \/ {x} c= F₂() by A5, XBOOLE_1:8;
then A10: B \/ {x} in GA by A4, A9;
not x in B by A7, XBOOLE_0:def 5;
then not {x} c= B by ZFMISC_1:37;
then ( B c= B \/ {x} & B \/ {x} <> B ) by XBOOLE_1:7;
hence contradiction by A5, A10; :: thesis: verum

end;

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

end;

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