for A being set
for R being Relation of A
for E being Equivalence_Relation of A st R c= E holds
for a, b being object st a in A & a,b are_convertible_wrt R holds
[a,b] in E