theorem Th55: :: GFACIRC1:55

for x, y, z being set holds InnerVertices (GFA1AdderStr (x,y,z)) = {[<*x,y*>,xor2c]} \/ {(GFA1AdderOutput (x,y,z))}