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