theorem Th40: :: FACIRC_1:40

for f, x, y being object holds InputVertices (1GateCircStr (<*x,y*>,f)) = {x,y}