[<*[<*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