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