for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being SortSymbol of IIG holds size (v,A) > 0