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₁() 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, Th18;
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 A9: x in F₁() by XBOOLE_0:def 5;
then A10: P₁[B \/ {x}] by A3, A5, A7;
{x} c= F₁() by A9, ZFMISC_1:37;
then B \/ {x} c= F₁() by A5, XBOOLE_1:8;
then A11: B \/ {x} in GA by A4, A10;
not x in B by A8, XBOOLE_0:def 5;
then not {x} c= B by ZFMISC_1:37;
then B \/ {x} <> B by XBOOLE_1:7;
hence contradiction by A6, A11, XBOOLE_1:7; :: thesis: verum

end;

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

end;

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