:: deftheorem defines -CircuitStr CIRCTRM1:def 1 :
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 = ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #);