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