set S = { [F₃(x),F₄(x)] where x is Element of F₁() : P₁[x] } ;
{ [F₃(x),F₄(x)] where x is Element of F₁() : P₁[x] } is Relation-like

proof

let x be set ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [F₃(x),F₄(x)] where x is Element of F₁() : P₁[x] } or ex b₁, b₂ being set st x = [b₁,b₂] )
assume x in { [F₃(x),F₄(x)] where x is Element of F₁() : P₁[x] } ; :: thesis: ex b₁, b₂ being set st x = [b₁,b₂]
then ex y being Element of F₁() st
( x = [F₃(y),F₄(y)] & P₁[y] ) ;
hence ex b₁, b₂ being set st x = [b₁,b₂] ; :: thesis: verum

end;

then reconsider S9 = { [F₃(x),F₄(x)] where x is Element of F₁() : P₁[x] } as Relation ;
A2: for x, y being set st [y,x] in F₂() holds
[x,y] in S9

proof

let x, y be set ; :: thesis: ( [y,x] in F₂() implies [x,y] in S9 )
assume [y,x] in F₂() ; :: thesis: [x,y] in S9
then consider z being Element of F₁() such that
A3: [y,x] = [F₄(z),F₃(z)] and
A4: P₁[z] by A1;
( y = F₄(z) & x = F₃(z) ) by A3, ZFMISC_1:33;
hence [x,y] in S9 by A4; :: thesis: verum

end;

for x, y being set st [x,y] in S9 holds
[y,x] in F₂()

proof

let x, y be set ; :: thesis: ( [x,y] in S9 implies [y,x] in F₂() )
assume [x,y] in S9 ; :: thesis: [y,x] in F₂()
then consider z being Element of F₁() such that
A5: [x,y] = [F₃(z),F₄(z)] and
A6: P₁[z] ;
( x = F₃(z) & y = F₄(z) ) by A5, ZFMISC_1:33;
hence [y,x] in F₂() by A1, A6; :: thesis: verum

end;

hence F₂() ~ = { [F₃(x),F₄(x)] where x is Element of F₁() : P₁[x] } by A2, RELAT_1:def 7; :: thesis: verum