theorem Th13: :: FACIRC_2:13

for n, m being Element of NAT st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices (m -BitAdderStr (x,y))