set S = { [F3(x),F4(x)] where x is Element of F1() : P1[x] } ;
{ [F3(x),F4(x)] where x is Element of F1() : P1[x] } is Relation-like
proof
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [F3(x),F4(x)] where x is Element of F1() : P1[x] } or ex b1, b2 being object st x = [b1,b2] )
assume x in { [F3(x),F4(x)] where x is Element of F1() : P1[x] } ; :: thesis: ex b1, b2 being object st x = [b1,b2]
then ex y being Element of F1() st
( x = [F3(y),F4(y)] & P1[y] ) ;
hence ex b1, b2 being object st x = [b1,b2] ; :: thesis: verum
end;
then reconsider S9 = { [F3(x),F4(x)] where x is Element of F1() : P1[x] } as Relation ;
A2: for x, y being object st [y,x] in F2() holds
[x,y] in S9
proof
let x, y be object ; :: thesis: ( [y,x] in F2() implies [x,y] in S9 )
assume [y,x] in F2() ; :: thesis: [x,y] in S9
then consider z being Element of F1() such that
A3: [y,x] = [F4(z),F3(z)] and
A4: P1[z] by A1;
( y = F4(z) & x = F3(z) ) by A3, XTUPLE_0:1;
hence [x,y] in S9 by A4; :: thesis: verum
end;
for x, y being object st [x,y] in S9 holds
[y,x] in F2()
proof
let x, y be object ; :: thesis: ( [x,y] in S9 implies [y,x] in F2() )
assume [x,y] in S9 ; :: thesis: [y,x] in F2()
then consider z being Element of F1() such that
A5: [x,y] = [F3(z),F4(z)] and
A6: P1[z] ;
 ( x = F3(z) & y = F4(z) ) by A5, XTUPLE_0:1;
hence [y,x] in F2() by A1, A6; :: thesis: verum
end;
hence F2() ~ = { [F3(x),F4(x)] where x is Element of F1() : P1[x] } by A2, RELAT_1:def 7; :: thesis: verum