:: deftheorem defines leq AOFA_A00:def 46 :
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 the Sorts of A . I holds leq (a,b) = (Den ((In (( the connectives of S . 10), the carrier' of S)),A)) . <*a,b*>;