theorem Th47: :: FACIRC_1:47

for p being FinSequence
for f being set holds [p,f] in InnerVertices (1GateCircStr (p,f))