theorem Th75: :: GFACIRC1:75

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