GFA3CarryOutput x,y,z in InnerVertices (BitGFA3Str x,y,z) by Th156;
hence [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] is Element of InnerVertices (BitGFA3Str x,y,z) ; :: thesis: verum