for A being non empty set
for R being Relation of A
for a, b being Element of A holds
( [a,b] in EqCl R iff a,b are_convertible_wrt R )