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