let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1
let G2 be removeDParallelEdges of G1; :: thesis: for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1
let G3 be removeLoops of G2; :: thesis: G3 is DSimpleGraph of G1
consider E being RepDEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def8;
A2: ( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;
then A3: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E ) by A1, GLIB_000:def 37;
A4: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 = (the_Edges_of G2) \ (G2 .loops()) ) by GLIB_000:53;
A5: (the_Edges_of G2) \ (G1 .loops()) c= (the_Edges_of G2) \ (G2 .loops()) by Th48, XBOOLE_1:34;

now :: thesis: for e being object st e in (the_Edges_of G2) \ (G2 .loops()) holds
e in (the_Edges_of G2) \ (G1 .loops())

let e be object ; :: thesis: ( e in (the_Edges_of G2) \ (G2 .loops()) implies e in (the_Edges_of G2) \ (G1 .loops()) )
assume e in (the_Edges_of G2) \ (G2 .loops()) ; :: thesis: e in (the_Edges_of G2) \ (G1 .loops())
then A6: ( e in the_Edges_of G2 & not e in G2 .loops() ) by XBOOLE_0:def 5;
not e in G1 .loops()

proof

assume e in G1 .loops() ; :: thesis: contradiction
then consider v being object such that
A7: e Joins v,v,G1 by Def2;
( e is set & v is set ) by TARSKI:1;
then e Joins v,v,G2 by A6, A7, GLIB_000:73;
hence contradiction by A6, Def2; :: thesis: verum

end;

hence e in (the_Edges_of G2) \ (G1 .loops()) by A6, XBOOLE_0:def 5; :: thesis: verum

end;

then (the_Edges_of G2) \ (G2 .loops()) c= (the_Edges_of G2) \ (G1 .loops()) by TARSKI:def 3;
then A8: the_Edges_of G3 = E \ (G1 .loops()) by A3, A4, A5, XBOOLE_0:def 10;
A9: the_Vertices_of G3 = the_Vertices_of G1 by A3, A4;
G3 is Subgraph of G1 by GLIB_000:43;
then G3 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops()) by A2, A8, A9, GLIB_000:def 37;
hence G3 is DSimpleGraph of G1 by Def10; :: thesis: verum