theorem Th58: :: FACIRC_1:58

for x, y, c being object
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) is Relation