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())
; 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
; 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())
; verum