set p = <*[<*x,y*>,f],c*>;
set S1 = 1GateCircStr <*x,y*>,f;
set S2 = 1GateCircStr <*[<*x,y*>,f],c*>,f;
( [<*[<*x,y*>,f],c*>,f] in InnerVertices (1GateCircStr <*[<*x,y*>,f],c*>,f) & 2GatesCircStr x,y,c,f = (1GateCircStr <*x,y*>,f) +* (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