let x, b be non pair set ; :: thesis: ( [<*x,b*>,xor2a ] in InnerVertices (BitCompStr x,b) & [<*x,b*>,and2a ] in InnerVertices (BitCompStr x,b) )
InnerVertices (BitCompStr x,b) = {[<*x,b*>,xor2a ],[<*x,b*>,and2a ]} by Th49;
hence ( [<*x,b*>,xor2a ] in InnerVertices (BitCompStr x,b) & [<*x,b*>,and2a ] in InnerVertices (BitCompStr x,b) ) by TARSKI:def 2; :: thesis: verum