theorem Th5: :: CIRCTRM1:5

for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )