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:42;
hence [<*x,b*>,xor2a] in InnerVertices (CompStr (x,b)) by TARSKI:def 1; :: thesis: verum