InputVertices (1GateCircStr (p,f)) = rng p by CIRCCOMB:49;
hence not InputVertices (1GateCircStr (p,f)) is with_pair ; :: according to CIRCCMB3:def 11 :: thesis: verum