:: deftheorem defines Equations EQUATION:def 4 :
for S being non empty non void ManySortedSign holds Equations S = [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];