for n, m being Nat st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y))