set E = the RepDEdgeSelection of G;
reconsider G2 = the plain inducedSubgraph of G, the_Vertices_of G, the RepDEdgeSelection of G \ (G .loops()) as DSimpleGraph of G by Def10;
take G2 ; :: thesis: G2 is plain
thus G2 is plain ; :: thesis: verum