theorem Th57: :: FACIRC_1:57

for x, y, c being object
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st c <> [<*x,y*>,f] holds
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}