set S1 = 1GateCircStr <*x,y*>,f;
set p = <*[<*x,y*>,f],c*>;
set S2 = 1GateCircStr <*[<*x,y*>,f],c*>,f;
[<*[<*x,y*>,f],c*>,f] in InnerVertices (1GateCircStr <*[<*x,y*>,f],c*>,f) by Th47;
hence [<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr x,y,c,f) by Th21; :: thesis: verum