for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t1, t2 being Element of (TermAlg S),s st A |= t1 '=' t2 holds
A |= t2 '=' t1 ;