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