consider Y being set such that
A3: for x being set holds
( x in Y iff ( x in F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
A4: ex x being set st x in Y

proof

consider x being set such that
A5: ( x in F₁() & P₁[x] ) by A2;
take x ; :: thesis: x in Y
thus x in Y by A3, A5; :: thesis: verum

end;

for x being set st x in Y holds
x in F₁() by A3;
then Y c= F₁() by TARSKI:def 3;
then consider X being set such that
A6: X in Y and
A7: for Z being set st Z in Y holds
[X,Z] in F₂() by A1, A4, WELLORD1:5;
A8: for M being set st M in F₁() & P₁[M] holds
[X,M] in F₂()

proof

let M be set ; :: thesis: ( M in F₁() & P₁[M] implies [X,M] in F₂() )
assume ( M in F₁() & P₁[M] ) ; :: thesis: [X,M] in F₂()
then M in Y by A3;
hence [X,M] in F₂() by A7; :: thesis: verum

end;

( X in F₁() & P₁[X] ) by A3, A6;
hence ex X being set st
( X in F₁() & P₁[X] & ( for Y being set st Y in F₁() & P₁[Y] holds
[X,Y] in F₂() ) ) by A8; :: thesis: verum