theorem Th43: :: GFACIRC1:43

for x, y, z being set holds InnerVertices (GFA1CarryStr (x,y,z)) is Relation