let x, b be non pair set ; :: thesis: [<*x,b*>,xor2a ] in InnerVertices (CompStr x,b)
InnerVertices (CompStr x,b) = {[<*x,b*>,xor2a ]} by CIRCCOMB:49;
hence [<*x,b*>,xor2a ] in InnerVertices (CompStr x,b) by TARSKI:def 1; :: thesis: verum