theorem Th57: :: GFACIRC1:57

for x, y, z being set holds
( [<*x,y*>,xor2c] in InnerVertices (GFA1AdderStr (x,y,z)) & GFA1AdderOutput (x,y,z) in InnerVertices (GFA1AdderStr (x,y,z)) )