theorem :: FACIRC_1:39

for f being set
for p being nonpair-yielding FinSequence holds InputVertices (1GateCircStr (p,f)) is without_pairs