let x, y, z be set ; :: thesis: InnerVertices (GFA0AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA0AdderOutput (x,y,z))}
set f = xor2 ;
set xy = [<*x,y*>,xor2];
set S = GFA0AdderStr (x,y,z);
thus InnerVertices (GFA0AdderStr (x,y,z)) = {[<*x,y*>,xor2],(GFA0AdderOutput (x,y,z))} by FACIRC_1:56
.= {[<*x,y*>,xor2]} \/ {(GFA0AdderOutput (x,y,z))} by ENUMSET1:1 ; :: thesis: verum