theorem :: FACIRC_2:16

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