theorem Th50: :: GFACIRC1:50
for x, y, z being non pair set holds InputVertices (GFA1CarryStr (x,y,z)) = {x,y,z}