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 ;
RELAT_2:def 8 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 ;
( 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 )
;
[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;
verum
end;
A9:
Y is_symmetric_in F1()
proof
let x be
object ;
RELAT_2:def 3 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 ;
( 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
;
[y,x] in Y
P1[
x,
y]
by A4, A11;
then
P1[
y,
x]
by A2;
hence
[y,x] in Y
by A4, A10;
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
; 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; verum