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 x being set holds
( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) )