let G1 be _Graph; :: thesis: for G3 being SimpleGraph of G1 ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2
let G3 be SimpleGraph of G1; :: thesis: ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops()) by Def9;
set G2 = the inducedSubgraph of G1, the_Vertices_of G1,E;
reconsider G2 = the inducedSubgraph of G1, the_Vertices_of G1,E as removeParallelEdges of G1 by Def7;
take G2 ; :: thesis: 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()) )

proof

let e be object ; :: thesis: ( e in the_Edges_of G3 iff e in (the_Edges_of G2) \ (G2 .loops()) )

hereby :: thesis: ( e in (the_Edges_of G2) \ (G2 .loops()) implies e in the_Edges_of G3 )

assume e in the_Edges_of G3 ; :: thesis: e in (the_Edges_of G2) \ (G2 .loops())
then A6: ( e in the_Edges_of G2 & not e in G1 .loops() ) by A3, A4, XBOOLE_0:def 5;
not e in G2 .loops()

proof

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

end;

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

end;

assume e in (the_Edges_of G2) \ (G2 .loops()) ; :: thesis: e in the_Edges_of G3
then A8: ( 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
A9: e Joins v,v,G1 by Def2;
( e is set & v is set ) by TARSKI:1;
then e Joins v,v,G2 by A8, A9, GLIB_000:73;
hence contradiction by A8, Def2; :: thesis: verum

end;

hence e in the_Edges_of G3 by A3, A4, A8, XBOOLE_0:def 5; :: thesis: verum

end;

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; :: thesis: verum