for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e