set E = the RepEdgeSelection of G;
reconsider G2 = the plain inducedSubgraph of G, the_Vertices_of G, the RepEdgeSelection of G as removeParallelEdges of G by Def7;
take G2 ; :: thesis: G2 is plain
thus G2 is plain ; :: thesis: verum