consider Y being Relation of F₁(),F₁() such that
A4: for x, y being set holds
( [x,y] in Y iff ( x in F₁() & y in F₁() & P₁[x,y] ) ) from RELSET_1:sch 1();
A5: Y is_reflexive_in F₁()

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in F₁() or [x,x] in Y )
assume A6: x in F₁() ; :: thesis: [x,x] in Y
then P₁[x,x] by A1;
hence [x,x] in Y by A4, A6; :: thesis: verum

end;

A7: Y is_symmetric_in F₁()

proof

let x be set ; :: according to RELAT_2:def 3 :: thesis: for b₁ being set holds
( not x in F₁() or not b₁ in F₁() or not [x,b₁] in Y or [b₁,x] in Y )
let y be set ; :: thesis: ( not x in F₁() or not y in F₁() or not [x,y] in Y or [y,x] in Y )
assume A8: ( x in F₁() & y in F₁() & [x,y] in Y ) ; :: thesis: [y,x] in Y
then P₁[x,y] by A4;
then ( y in F₁() & x in F₁() & P₁[y,x] ) by A2, A8;
hence [y,x] in Y by A4; :: thesis: verum

end;

A9: Y is_transitive_in F₁()

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in F₁() or not b₁ in F₁() or not b₂ in F₁() or not [x,b₁] in Y or not [b₁,b₂] in Y or [x,b₂] in Y )
let y, z be set ; :: thesis: ( not x in F₁() or not y in F₁() or not z in F₁() or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )
assume A10: ( x in F₁() & y in F₁() & z in F₁() & [x,y] in Y & [y,z] in Y ) ; :: thesis: [x,z] in Y
then A11: P₁[x,y] by A4;
P₁[y,z] by A4, A10;
then P₁[x,z] by A3, A11;
hence [x,z] in Y by A4, A10; :: thesis: verum

end;

A12: field Y = F₁() by A5, ORDERS_1:98;
dom Y = F₁() by A5, ORDERS_1:98;
then reconsider R1 = Y as Equivalence_Relation of F₁() by A7, A9, A12, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
take R1 ; :: thesis: for x, y being set holds
( [x,y] in R1 iff ( x in F₁() & y in F₁() & P₁[x,y] ) )
thus for x, y being set holds
( [x,y] in R1 iff ( x in F₁() & y in F₁() & P₁[x,y] ) ) by A4; :: thesis: verum