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:42;
hence not InputVertices (1GateCircStr (p,f)) is with_pair ; :: thesis: verum