now :: thesis: ( F₁() <> {} implies P₁[F₁()] )

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 XFAMILY:sch 1();
G c= bool F₁() by A4;
then reconsider GA = G as Subset-Family of F₁() ;
{} c= F₁() ;
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, Th6;
A7: ex A being set st
( A = B & P₁[A] ) by A4, A5;

now :: thesis: not B <> F₁()

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