let A be set ; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: ( E is total & E is symmetric & E is transitive )

now :: thesis: for x being object st x in A holds
[x,x] in E

let x be object ; :: thesis: ( x in A implies [x,x] in E )
x,x are_convertible_wrt R by REWRITE1:26;
hence ( x in A implies [x,x] in E ) by A1; :: thesis: verum

end;

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; :: thesis: ( E is symmetric & E is transitive )

now :: thesis: for x, y being object st x in A & y in A & [x,y] in E holds
[y,x] in E

let x, y be object ; :: thesis: ( 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 ; :: thesis: ( [x,y] in E implies [y,x] in E )
assume [x,y] in E ; :: thesis: [y,x] in E
then 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; :: thesis: verum

end;

then E is_symmetric_in A by RELAT_2:def 3;
hence E is symmetric by A3, RELAT_2:def 11; :: thesis: E is transitive

now :: thesis: 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 E

let x, y, z be object ; :: thesis: ( 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 ; :: thesis: ( [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 ; :: thesis: [x,z] in E
A11: 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; :: thesis: verum

end;

then E is_transitive_in A by RELAT_2:def 8;
hence E is transitive by A3, RELAT_2:def 16; :: thesis: verum