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