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