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