ex R being Relation st
for p being set holds
( p in R iff ( p in [:F₁(),F₂():] & ex x, y being set st
( p = [x,y] & P₁[x,y] ) ) )

proof

defpred S₁[ set ] means ex x, y being set st
( $1 = [x,y] & P₁[x,y] );
consider B being set such that
A1: for p being set holds
( p in B iff ( p in [:F₁(),F₂():] & S₁[p] ) ) from XBOOLE_0:sch 1();
for p being set st p in B holds
ex x, y being set st p = [x,y]

proof

let p be set ; :: thesis: ( p in B implies ex x, y being set st p = [x,y] )
assume p in B ; :: thesis: ex x, y being set st p = [x,y]
then ex x, y being set st
( p = [x,y] & P₁[x,y] ) by A1;
hence ex x, y being set st p = [x,y] ; :: thesis: verum

end;

then B is Relation by Def1;
hence ex R being Relation st
for p being set holds
( p in R iff ( p in [:F₁(),F₂():] & ex x, y being set st
( p = [x,y] & P₁[x,y] ) ) ) by A1; :: thesis: verum

end;

then consider R being Relation such that
A2: for p being set holds
( p in R iff ( p in [:F₁(),F₂():] & ex x, y being set st
( p = [x,y] & P₁[x,y] ) ) ) ;
take R ; :: thesis: for x, y being set holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) )
let x, y be set ; :: thesis: ( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) )
thus ( [x,y] in R implies ( x in F₁() & y in F₂() & P₁[x,y] ) ) :: thesis: ( x in F₁() & y in F₂() & P₁[x,y] implies [x,y] in R )

proof

assume A3: [x,y] in R ; :: thesis: ( x in F₁() & y in F₂() & P₁[x,y] )
then consider xx, yy being set such that
A4: [x,y] = [xx,yy] and
A5: P₁[xx,yy] by A2;
A6: [x,y] in [:F₁(),F₂():] by A2, A3;
x = xx by A4, ZFMISC_1:27;
hence ( x in F₁() & y in F₂() & P₁[x,y] ) by A4, A5, A6, ZFMISC_1:27, ZFMISC_1:87; :: thesis: verum

end;

thus ( x in F₁() & y in F₂() & P₁[x,y] implies [x,y] in R ) :: thesis: verum

proof

assume that
A7: ( x in F₁() & y in F₂() ) and
A8: P₁[x,y] ; :: thesis: [x,y] in R
[x,y] in [:F₁(),F₂():] by A7, ZFMISC_1:87;
hence [x,y] in R by A2, A8; :: thesis: verum

end;