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