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()) )

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

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

then A10:
the_Edges_of G3 = (the_Edges_of G2) \ (G2 .loops())
by TARSKI:2;
let e be object ; :: thesis: ( e in the_Edges_of G3 iff e in (the_Edges_of G2) \ (G2 .loops()) )

then A8: ( e in the_Edges_of G2 & not e in G2 .loops() ) by XBOOLE_0:def 5;

not e in G1 .loops()

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

assume
e in (the_Edges_of G2) \ (G2 .loops())
; :: thesis: e in the_Edges_of G3assume
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()

end;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

hence
e in (the_Edges_of G2) \ (G2 .loops())
by A6, XBOOLE_0:def 5; :: thesis: verum
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;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

then A8: ( e in the_Edges_of G2 & not e in G2 .loops() ) by XBOOLE_0:def 5;

not e in G1 .loops()

proof

hence
e in the_Edges_of G3
by A3, A4, A8, XBOOLE_0:def 5; :: thesis: verum
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;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

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