let x, y, z be set ; :: thesis: ( [<*x,y*>,xor2] in InnerVertices (GFA0AdderStr (x,y,z)) & GFA0AdderOutput (x,y,z) in InnerVertices (GFA0AdderStr (x,y,z)) )
set f = xor2 ;
set S = GFA0AdderStr (x,y,z);
InnerVertices (GFA0AdderStr (x,y,z)) = {[<*x,y*>,xor2]} \/ {(GFA0AdderOutput (x,y,z))} by Th24
.= {[<*x,y*>,xor2],(GFA0AdderOutput (x,y,z))} by ENUMSET1:1 ;
hence ( [<*x,y*>,xor2] in InnerVertices (GFA0AdderStr (x,y,z)) & GFA0AdderOutput (x,y,z) in InnerVertices (GFA0AdderStr (x,y,z)) ) by TARSKI:def 2; :: thesis: verum