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