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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: verum

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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: verum