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) holds
( X -CircuitStr is void iff for t being Element of X holds
( t is root & not t . {} in [: the carrier' of S,{ the carrier of S}:] ) ) by TREES_9:25;