theorem Th41: :: TWOSCOMP:41

for x, b being non pair set holds
( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) )