theorem Th11: :: GFACIRC1:11

for x, y, z being set holds InnerVertices (GFA0CarryStr (x,y,z)) = {[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]} \/ {(GFA0CarryOutput (x,y,z))}