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