theorem Th87: :: GFACIRC1:87

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