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

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

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

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

consider E being RepEdgeSelection of G2 such that

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

( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween (the_Vertices_of G2) ) by GLIB_000:34;

then A2: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 = E ) by A1, GLIB_000:def 37;

A3: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ (G1 .loops()) ) by GLIB_000:53;

consider E0 being RepEdgeSelection of G1 such that

A4: E = E0 /\ (the_Edges_of G2) by Th80;

A5: the_Vertices_of G3 = the_Vertices_of G1 by A2, A3;

for e being object holds

( e in the_Edges_of G3 iff e in E0 \ (G1 .loops()) )

A10: G3 is Subgraph of G1 by GLIB_000:43;

( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;

then G3 is inducedSubgraph of G1, the_Vertices_of G1,E0 \ (G1 .loops()) by A5, A9, A10, GLIB_000:def 37;

hence G3 is SimpleGraph of G1 by Def9; :: thesis: verum

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

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

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

consider E being RepEdgeSelection of G2 such that

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

( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween (the_Vertices_of G2) ) by GLIB_000:34;

then A2: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 = E ) by A1, GLIB_000:def 37;

A3: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ (G1 .loops()) ) by GLIB_000:53;

consider E0 being RepEdgeSelection of G1 such that

A4: E = E0 /\ (the_Edges_of G2) by Th80;

A5: the_Vertices_of G3 = the_Vertices_of G1 by A2, A3;

for e being object holds

( e in the_Edges_of G3 iff e in E0 \ (G1 .loops()) )

proof

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

then A8: e in the_Edges_of G2 by A3, TARSKI:def 3, XBOOLE_1:33;

e in E0 by A7, XBOOLE_0:def 5;

hence e in the_Edges_of G3 by A2, A4, A8, XBOOLE_0:def 4; :: thesis: verum

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

assume A7:
e in E0 \ (G1 .loops())
; :: thesis: e in the_Edges_of G3assume
e in the_Edges_of G3
; :: thesis: e in E0 \ (G1 .loops())

then A6: ( e in E0 & e in the_Edges_of G2 ) by A2, A4, XBOOLE_0:def 4;

then not e in G1 .loops() by A3, XBOOLE_0:def 5;

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

end;then A6: ( e in E0 & e in the_Edges_of G2 ) by A2, A4, XBOOLE_0:def 4;

then not e in G1 .loops() by A3, XBOOLE_0:def 5;

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

then A8: e in the_Edges_of G2 by A3, TARSKI:def 3, XBOOLE_1:33;

e in E0 by A7, XBOOLE_0:def 5;

hence e in the_Edges_of G3 by A2, A4, A8, XBOOLE_0:def 4; :: thesis: verum

A10: G3 is Subgraph of G1 by GLIB_000:43;

( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;

then G3 is inducedSubgraph of G1, the_Vertices_of G1,E0 \ (G1 .loops()) by A5, A9, A10, GLIB_000:def 37;

hence G3 is SimpleGraph of G1 by Def9; :: thesis: verum