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