theorem Th74: :: GFACIRC1:74

for x, y, z being set holds InnerVertices (GFA2CarryStr (x,y,z)) = {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]} \/ {(GFA2CarryOutput (x,y,z))}