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 Th38;
hence ( [<*x,b*>,xor2a] in InnerVertices (BitCompStr (x,b)) & [<*x,b*>,and2a] in InnerVertices (BitCompStr (x,b)) ) by TARSKI:def 2; :: thesis: verum