:: deftheorem defines - AOFA_A00:def 47 :
for S being non empty non void 4,1 integer BoolSignature
for A being non-empty MSAlgebra over S
for I being integer SortSymbol of S
for a, b being Element of A,I holds a - b = a + (- b);