theorem Th8: :: FSCIRC_2:8

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