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