theorem :: FSCIRC_2:11

for n being Element of NAT
for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) is Relation