for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A
for s being SortSymbol of S
for a, b being Element of A,s holds
( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s )