let f be set ; :: thesis: for x, y being set holds InputVertices (1GateCircStr <*x,y*>,f) = {x,y}
let x, y be set ; :: thesis: InputVertices (1GateCircStr <*x,y*>,f) = {x,y}
set p = <*x,y*>;
thus InputVertices (1GateCircStr <*x,y*>,f) = rng <*x,y*> by CIRCCOMB:49
.= {x,y} by FINSEQ_2:147 ; :: thesis: verum