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 Th63
.= {[<*x,y*>,xor2c ],(GFA1AdderOutput x,y,z)} by ENUMSET1:41 ;
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