consider Y being Relation of F_{1}(),F_{1}() such that

A4: for x, y being object holds

( [x,y] in Y iff ( x in F_{1}() & y in F_{1}() & P_{1}[x,y] ) )
from RELSET_1:sch 1();

A5: Y is_transitive_in F_{1}()
_{1}()
_{1}()
by A1, A4;

then ( field Y = F_{1}() & dom Y = F_{1}() )
by ORDERS_1:13;

then reconsider R1 = Y as Equivalence_Relation of F_{1}() 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 F_{1}() & y in F_{1}() & P_{1}[x,y] ) )

thus for x, y being object holds

( [x,y] in R1 iff ( x in F_{1}() & y in F_{1}() & P_{1}[x,y] ) )
by A4; :: thesis: verum

A4: for x, y being object holds

( [x,y] in Y iff ( x in F

A5: Y is_transitive_in F

proof

A9:
Y is_symmetric_in F
let x be object ; :: according to RELAT_2:def 8 :: thesis: for b_{1}, b_{2} being object holds

( not x in F_{1}() or not b_{1} in F_{1}() or not b_{2} in F_{1}() or not [x,b_{1}] in Y or not [b_{1},b_{2}] in Y or [x,b_{2}] in Y )

let y, z be object ; :: thesis: ( not x in F_{1}() or not y in F_{1}() or not z in F_{1}() or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )

assume that

A6: x in F_{1}()
and

y in F_{1}()
and

A7: z in F_{1}()
and

A8: ( [x,y] in Y & [y,z] in Y ) ; :: thesis: [x,z] in Y

( P_{1}[x,y] & P_{1}[y,z] )
by A4, A8;

then P_{1}[x,z]
by A3;

hence [x,z] in Y by A4, A6, A7; :: thesis: verum

end;( not x in F

let y, z be object ; :: thesis: ( not x in F

assume that

A6: x in F

y in F

A7: z in F

A8: ( [x,y] in Y & [y,z] in Y ) ; :: thesis: [x,z] in Y

( P

then P

hence [x,z] in Y by A4, A6, A7; :: thesis: verum

proof

Y is_reflexive_in F
let x be object ; :: according to RELAT_2:def 3 :: thesis: for b_{1} being object holds

( not x in F_{1}() or not b_{1} in F_{1}() or not [x,b_{1}] in Y or [b_{1},x] in Y )

let y be object ; :: thesis: ( not x in F_{1}() or not y in F_{1}() or not [x,y] in Y or [y,x] in Y )

assume that

A10: ( x in F_{1}() & y in F_{1}() )
and

A11: [x,y] in Y ; :: thesis: [y,x] in Y

P_{1}[x,y]
by A4, A11;

then P_{1}[y,x]
by A2;

hence [y,x] in Y by A4, A10; :: thesis: verum

end;( not x in F

let y be object ; :: thesis: ( not x in F

assume that

A10: ( x in F

A11: [x,y] in Y ; :: thesis: [y,x] in Y

P

then P

hence [y,x] in Y by A4, A10; :: thesis: verum

then ( field Y = F

then reconsider R1 = Y as Equivalence_Relation of F

take R1 ; :: thesis: for x, y being object holds

( [x,y] in R1 iff ( x in F

thus for x, y being object holds

( [x,y] in R1 iff ( x in F