for A being 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 )