theorem Th12: :: GFACIRC1:12

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