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