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