consider Y being Relation of F1(),F1() such that
A4: for x, y being object 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 object ; :: according to RELAT_2:def 8 :: thesis: for b1, b2 being object 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 object ; :: 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 object ; :: according to RELAT_2:def 3 :: thesis: for b1 being object holds
( not x in F1() or not b1 in F1() or not [x,b1] in Y or [b1,x] in Y )
let y be object ; :: 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() by A1, A4;
then ( field Y = F1() & dom Y = F1() ) by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of F1() by A9, A5, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
take R1 ; :: thesis: for x, y being object holds
( [x,y] in R1 iff ( x in F1() & y in F1() & P1[x,y] ) )
thus for x, y being object holds
( [x,y] in R1 iff ( x in F1() & y in F1() & P1[x,y] ) ) by A4; :: thesis: verum