:: deftheorem Def31 defines bool-correct AOFA_A00:def 31 :
for S being non empty non void BoolSignature
for B being MSAlgebra over S holds
( B is bool-correct iff ( the Sorts of B . the bool-sort of S = BOOLEAN & (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> = x '&' y ) ) ) );