for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]