theorem :: TWOSCOMP:32

for x, b being non pair set holds [<*x,b*>,and2a] in InnerVertices (IncrementStr (x,b))