consider X being set such that
A1: for x being set holds
( x in X iff ( x in F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
X c= F₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in F₁() )
thus ( not x in X or x in F₁() ) by A1; :: thesis: verum

end;

then X in bool F₁() by ZFMISC_1:def 1;
then reconsider X = X as Subset of F₁() by Def2;
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