theorem Th37: :: TWOSCOMP:37

for x, b being non pair set holds the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]}