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