let x, y, z be set ; InnerVertices (GFA3AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}
GFA3AdderOutput (x,y,z) = GFA0AdderOutput (x,y,z)
;
hence
InnerVertices (GFA3AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}
by Th24; verum