theorem :: GFACIRC1:64

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