:: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def 4 :
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being MSAlgebra over S
for b₅ being ManySortedSet of the carrier of (X -CircuitStr) holds
( b₅ = X -CircuitSorts A iff for v being Vertex of (X -CircuitStr) holds b₅ . v = the_sort_of (v,A) );