consider X being set such that
A1: for x being object holds
( x in X iff ( x in F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
X c= F₁() by A1;
then X in bool F₁() by ZFMISC_1:def 1;
then reconsider X = X as Subset of F₁() by Def1;
take X ; :: thesis: for x being set holds
( x in X iff ( x in F₁() & P₁[x] ) )
thus for x being set holds
( x in X iff ( x in F₁() & P₁[x] ) ) by A1; :: thesis: verum