theorem :: TWOSCOMP:35

for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) is Relation