theorem :: GFACIRC2:25

for n being Nat
for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) is Relation