set E = the RepDEdgeSelection of G;
reconsider G2 = the plain inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G as removeDParallelEdges of G by Def8;
take G2 ; :: thesis: G2 is plain
thus G2 is plain ; :: thesis: verum