theorem Th22: :: GFACIRC2:22

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