theorem Th48: :: GFACIRC1:48

for x, y, z being set holds
( [<*x,y*>,and2c] in InnerVertices (GFA1CarryStr (x,y,z)) & [<*y,z*>,and2a] in InnerVertices (GFA1CarryStr (x,y,z)) & [<*z,x*>,and2] in InnerVertices (GFA1CarryStr (x,y,z)) & GFA1CarryOutput (x,y,z) in InnerVertices (GFA1CarryStr (x,y,z)) )