theorem Th106: :: GFACIRC1:106

for x, y, z being set holds InnerVertices (GFA3CarryStr (x,y,z)) = {[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]} \/ {(GFA3CarryOutput (x,y,z))}