let f be set ; :: thesis: for p being nonpair-yielding FinSequence holds not InputVertices (1GateCircStr p,f) is with_pair
let p be nonpair-yielding FinSequence; :: thesis: not InputVertices (1GateCircStr p,f) is with_pair
InputVertices (1GateCircStr p,f) = rng p by CIRCCOMB:49;
hence not InputVertices (1GateCircStr p,f) is with_pair ; :: thesis: verum