theorem Th24: :: GFACIRC1:24

for x, y, z being set holds InnerVertices (GFA0AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA0AdderOutput (x,y,z))}