theorem :: TWOSCOMP:28

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