consider B being set such that
A1: for x being set holds
( x in B iff ( x in F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
for x being set st x in B holds
x in F₁() by A1;
then reconsider B = B as Subset of F₁() by Lm2;
take B ; :: thesis: for x being Element of F₁() holds
( x in B iff P₁[x] )
let x be Element of F₁(); :: thesis: ( x in B iff P₁[x] )
x in F₁() by Def2;
hence ( x in B iff P₁[x] ) by A1; :: thesis: verum