let G1 be _Graph; :: thesis: for G2 being removeLoops of G1
for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1

let G2 be removeLoops of G1; :: thesis: for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1
let G3 be removeDParallelEdges of G2; :: thesis: G3 is DSimpleGraph of G1
consider E being RepDEdgeSelection of G2 such that
A1: G3 is inducedSubgraph of G2, the_Vertices_of G2,E by Def8;
( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween () ) by GLIB_000:34;
then A2: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 = E ) by ;
A3: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = () \ (G1 .loops()) ) by GLIB_000:53;
consider E0 being RepDEdgeSelection of G1 such that
A4: E = E0 /\ () by Th81;
A5: the_Vertices_of G3 = the_Vertices_of G1 by A2, A3;
for e being object holds
( e in the_Edges_of G3 iff e in E0 \ (G1 .loops()) )
proof
let e be object ; :: thesis: ( e in the_Edges_of G3 iff e in E0 \ (G1 .loops()) )
hereby :: thesis: ( e in E0 \ (G1 .loops()) implies e in the_Edges_of G3 )
assume e in the_Edges_of G3 ; :: thesis: e in E0 \ (G1 .loops())
then A6: ( e in E0 & e in the_Edges_of G2 ) by ;
then not e in G1 .loops() by ;
hence e in E0 \ (G1 .loops()) by ; :: thesis: verum
end;
assume A7: e in E0 \ (G1 .loops()) ; :: thesis:
then A8: e in the_Edges_of G2 by ;
e in E0 by ;
hence e in the_Edges_of G3 by ; :: thesis: verum
end;
then A9: the_Edges_of G3 = E0 \ (G1 .loops()) by TARSKI:2;
A10: G3 is Subgraph of G1 by GLIB_000:43;
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween () ) by GLIB_000:34;
then G3 is inducedSubgraph of G1, the_Vertices_of G1,E0 \ (G1 .loops()) by ;
hence G3 is DSimpleGraph of G1 by Def10; :: thesis: verum