let A be set ; for R, E being Relation of A st ( for a, b being set st a in A & b in A holds
( [a,b] in E iff a,b are_convertible_wrt R ) ) holds
( E is total & E is symmetric & E is transitive )
let R, E be Relation of A; ( ( for a, b being set st a in A & b in A holds
( [a,b] in E iff a,b are_convertible_wrt R ) ) implies ( E is total & E is symmetric & E is transitive ) )
set X = A;
assume A1:
for a, b being set st a in A & b in A holds
( [a,b] in E iff a,b are_convertible_wrt R )
; ( E is total & E is symmetric & E is transitive )
then A2:
E is_reflexive_in A
by RELAT_2:def 1;
then A3:
field E = A
by ORDERS_1:13;
dom E = A
by A2, ORDERS_1:13;
hence
E is total
by PARTFUN1:def 2; ( E is symmetric & E is transitive )
now for x, y being object st x in A & y in A & [x,y] in E holds
[y,x] in Elet x,
y be
object ;
( x in A & y in A & [x,y] in E implies [y,x] in E )assume that A4:
x in A
and A5:
y in A
;
( [x,y] in E implies [y,x] in E )assume
[x,y] in E
;
[y,x] in Ethen
x,
y are_convertible_wrt R
by A1, A4, A5;
then
y,
x are_convertible_wrt R
by REWRITE1:31;
hence
[y,x] in E
by A1, A4, A5;
verum end;
then
E is_symmetric_in A
by RELAT_2:def 3;
hence
E is symmetric
by A3, RELAT_2:def 11; E is transitive
now for x, y, z being object st x in A & y in A & z in A & [x,y] in E & [y,z] in E holds
[x,z] in Elet x,
y,
z be
object ;
( x in A & y in A & z in A & [x,y] in E & [y,z] in E implies [x,z] in E )assume that A6:
x in A
and A7:
y in A
and A8:
z in A
;
( [x,y] in E & [y,z] in E implies [x,z] in E )assume that A9:
[x,y] in E
and A10:
[y,z] in E
;
[x,z] in EA11:
y,
z are_convertible_wrt R
by A1, A7, A8, A10;
x,
y are_convertible_wrt R
by A1, A6, A7, A9;
then
x,
z are_convertible_wrt R
by A11, REWRITE1:30;
hence
[x,z] in E
by A1, A6, A8;
verum end;
then
E is_transitive_in A
by RELAT_2:def 8;
hence
E is transitive
by A3, RELAT_2:def 16; verum