theorem :: GFACIRC2:11

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