theorem Th15: :: CIRCCMB3:15

for S being one-gate ManySortedSign
for p being FinSequence
for x being set st S = 1GateCircStr (p,x) holds
Output S = [p,x]