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