[<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] in InnerVertices (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3)) by FACIRC_1:47;
hence [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] is Element of InnerVertices (GFA3CarryStr (x,y,z)) by FACIRC_1:21; :: thesis: verum