consider Y being set such that
A3:
for x being object holds
( x in Y iff ( x in F1() & P1[x] ) )
from XBOOLE_0:sch 1();
A4:
ex x being object st x in Y
by A2, A3;
for x being object st x in Y holds
x in F1()
by A3;
then
Y c= F1()
;
then consider X being object such that
A5:
X in Y
and
A6:
for Z being object st Z in Y holds
[X,Z] in F2()
by A1, A4, WELLORD1:5;
A7:
for M being set st M in F1() & P1[M] holds
[X,M] in F2()
by A3, A6;
( X in F1() & P1[X] )
by A3, A5;
hence
ex X being set st
( X in F1() & P1[X] & ( for Y being set st Y in F1() & P1[Y] holds
[X,Y] in F2() ) )
by A7; verum