let G1 be _Graph; for G3 being DSimpleGraph of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2
let G3 be DSimpleGraph of G1; ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2
consider E being RepDEdgeSelection of G1 such that
A1:
G3 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops())
by Def10;
set G2 = the inducedSubgraph of G1, the_Vertices_of G1,E;
reconsider G2 = the inducedSubgraph of G1, the_Vertices_of G1,E as removeDParallelEdges of G1 by Def8;
take
G2
; G3 is removeLoops of G2
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 G3 = the_Vertices_of G1 & the_Edges_of G3 = E \ (G1 .loops()) )
by A1, GLIB_000:def 37;
A4:
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E )
by A2, GLIB_000:def 37;
A5:
the_Vertices_of G3 = the_Vertices_of G2
by A3, A4;
for e being object holds
( e in the_Edges_of G3 iff e in (the_Edges_of G2) \ (G2 .loops()) )
then A10:
the_Edges_of G3 = (the_Edges_of G2) \ (G2 .loops())
by TARSKI:2;
E \ (G1 .loops()) c= E
by XBOOLE_1:36;
then A11:
G3 is Subgraph of G2
by A2, A1, GLIB_000:46;
( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween (the_Vertices_of G2) )
by GLIB_000:34;
hence
G3 is removeLoops of G2
by A5, A10, A11, GLIB_000:def 37; verum