theorem Th42: :: GFACIRC1:42

for x, y, z being set holds InnerVertices (GFA1CarryStr (x,y,z)) = {[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]} \/ {(GFA1CarryOutput (x,y,z))}