for S being non empty non void bool-correct BoolSignature
for A being V2() ManySortedSet of the carrier of S ex B being strict non-empty MSAlgebra over S st
( the Sorts of B = A +* ( the bool-sort of S,BOOLEAN) & B is bool-correct )