:: deftheorem defines |= EQUATION:def 6 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for E being EqualSet of S holds
( A |= E iff for s being SortSymbol of S
for e being Element of (Equations S) . s st e in E . s holds
A |= e );