theorem Th3: :: CIRCTRM1:3

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) holds
( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )