set E = the RepDEdgeSelection of G;

set G2 = the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops());

take the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) ; :: thesis: ex E being RepDEdgeSelection of G st the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())

take the RepDEdgeSelection of G ; :: thesis: the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) is inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops())

thus the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) is inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) ; :: thesis: verum

set G2 = the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops());

take the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) ; :: thesis: ex E being RepDEdgeSelection of G st the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())

take the RepDEdgeSelection of G ; :: thesis: the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) is inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops())

thus the inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) is inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) ; :: thesis: verum