theorem Th38: :: FACIRC_1:38

for f being set
for p being FinSequence holds InnerVertices (1GateCircStr (p,f)) is Relation