set E = the RepEdgeSelection of G;
set G2 = the inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G;
take
the inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G
; ex E being RepEdgeSelection of G st the inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G is inducedSubgraph of G, the_Vertices_of G,E
take
the RepEdgeSelection of G
; the inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G is inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G
thus
the inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G is inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G
; verum