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