let G1 be _Graph; :: thesis: for G2 being removeParallelEdges of G1

for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1

let G2 be removeParallelEdges of G1; :: thesis: for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1

let G3 be removeLoops of G2; :: thesis: G3 is SimpleGraph of G1

consider E being RepEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;

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;

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 SimpleGraph of G1 by Def9; :: thesis: verum

for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1

let G2 be removeParallelEdges of G1; :: thesis: for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1

let G3 be removeLoops of G2; :: thesis: G3 is SimpleGraph of G1

consider E being RepEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;

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

then
(the_Edges_of G2) \ (G2 .loops()) c= (the_Edges_of G2) \ (G1 .loops())
by TARSKI:def 3;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()

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

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

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 SimpleGraph of G1 by Def9; :: thesis: verum