let x, b be non pair set ; :: thesis: 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]} ; :: thesis: verum