let x, b be non pair set ; InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
set p = <*x,b*>;
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
set S = BitCompStr (x,b);
A1:
( InnerVertices (CompStr (x,b)) = {[<*x,b*>,xor2a]} & InnerVertices (IncrementStr (x,b)) = {[<*x,b*>,and2a]} )
by CIRCCOMB:42;
InnerVertices (BitCompStr (x,b)) =
(InnerVertices (CompStr (x,b))) \/ (InnerVertices (IncrementStr (x,b)))
by FACIRC_1:27
.=
{[<*x,b*>,xor2a],[<*x,b*>,and2a]}
by A1, ENUMSET1:1
;
hence
InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
; verum