theorem Th38: :: TWOSCOMP:38

for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]}