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:49;
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:41 ;
hence InnerVertices (BitCompStr x,b) = {[<*x,b*>,xor2a ],[<*x,b*>,and2a ]} ; :: thesis: verum