consider Y being Relation of F1(),F1() such that
A4: for x, y being set holds
( [x,y] in Y iff ( x in F1() & y in F1() & P1[x,y] ) ) from RELSET_1:sch 1();
 A5: Y is_transitive_in F1()
proof
let x be set ; :: according to RELAT_2:def 8 :: thesis: for b1, b2 being set holds
( not x in F1() or not b1 in F1() or not b2 in F1() or not [x,b1] in Y or not [b1,b2] in Y or [x,b2] in Y )
let y, z be set ; :: thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )
assume that
A6: x in F1() and
y in F1() and
A7: z in F1() and
A8: ( [x,y] in Y & [y,z] in Y ) ; :: thesis: [x,z] in Y
( P1[x,y] & P1[y,z] ) by A4, A8;
then P1[x,z] by A3;
hence [x,z] in Y by A4, A6, A7; :: thesis: verum
end;
A9: Y is_symmetric_in F1()
proof
let x be set ; :: according to RELAT_2:def 3 :: thesis: for b1 being set holds
( not x in F1() or not b1 in F1() or not [x,b1] in Y or [b1,x] in Y )
let y be set ; :: thesis: ( not x in F1() or not y in F1() or not [x,y] in Y or [y,x] in Y )
assume that
A10: ( x in F1() & y in F1() ) and
A11: [x,y] in Y ; :: thesis: [y,x] in Y
P1[x,y] by A4, A11;
then P1[y,x] by A2;
hence [y,x] in Y by A4, A10; :: thesis: verum
end;
Y is_reflexive_in F1()
proof
let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in F1() or [x,x] in Y )
assume A12: x in F1() ; :: thesis: [x,x] in Y
then P1[x,x] by A1;
hence [x,x] in Y by A4, A12; :: thesis: verum
end;
then ( field Y = F1() & dom Y = F1() ) by ORDERS_1:98;
then reconsider R1 = Y as Equivalence_Relation of F1() by A9, A5, 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 F1() & y in F1() & P1[x,y] ) )
thus for x, y being set holds
( [x,y] in R1 iff ( x in F1() & y in F1() & P1[x,y] ) ) by A4; :: thesis: verum