theorem :: TWOSCOMP:33
for x, b being non pair set holds
( x in InputVertices (IncrementStr (x,b)) & b in InputVertices (IncrementStr (x,b)) )