defpred S₁[ set ] means ex Z being set st
( $1 = Z & P₁[Z] );
consider X being set such that
A2: for x being set holds
( x in X iff ( x in bool F₁() & S₁[x] ) ) from XFAMILY:sch 1();
X c= bool F₁() by A2;
then reconsider X = X as non empty Subset-Family of F₁() by A1, A2;
take X ; :: thesis: for B being set holds
( B in X iff ( B c= F₁() & P₁[B] ) )
for B being set holds
( B in X iff ( B c= F₁() & P₁[B] ) )

proof

let B be set ; :: thesis: ( B in X iff ( B c= F₁() & P₁[B] ) )
thus ( B in X implies ( B c= F₁() & P₁[B] ) ) :: thesis: ( B c= F₁() & P₁[B] implies B in X )

proof

assume A3: B in X ; :: thesis: ( B c= F₁() & P₁[B] )
then ex Z being set st
( B = Z & P₁[Z] ) by A2;
hence ( B c= F₁() & P₁[B] ) by A3; :: thesis: verum

end;

assume ( B c= F₁() & P₁[B] ) ; :: thesis: B in X
hence B in X by A2; :: thesis: verum

end;

hence for B being set holds
( B in X iff ( B c= F₁() & P₁[B] ) ) ; :: thesis: verum