theorem Th16: :: CIRCCMB3:16

for S being one-gate ManySortedSign holds InnerVertices S = {(Output S)}