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

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

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

let G3 be SimpleGraph of G1; :: thesis: G3 is removeParallelEdges 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;

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 = (the_Edges_of G1) \ (G1 .loops()) ) by GLIB_000:53;

set E2 = E \ (G1 .loops());

A5: E \ (G1 .loops()) c= the_Edges_of G2 by A4, XBOOLE_1:33;

A14: the_Vertices_of G3 = the_Vertices_of G2 by A3, A4;

E \ (G1 .loops()) c= (the_Edges_of G1) \ (G1 .loops()) by XBOOLE_1:33;

then A15: G3 is Subgraph of G2 by A1, A2, 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;

then G3 is inducedSubgraph of G2, the_Vertices_of G2,E2 by A3, A14, A15, GLIB_000:def 37;

hence G3 is removeParallelEdges of G2 by Def7; :: thesis: verum

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

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

let G3 be SimpleGraph of G1; :: thesis: G3 is removeParallelEdges 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;

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 = (the_Edges_of G1) \ (G1 .loops()) ) by GLIB_000:53;

set E2 = E \ (G1 .loops());

A5: E \ (G1 .loops()) c= the_Edges_of G2 by A4, XBOOLE_1:33;

now :: thesis: for v, w, e0 being object st e0 Joins v,w,G2 holds

ex e being object st

( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

then reconsider E2 = E \ (G1 .loops()) as RepEdgeSelection of G2 by A5, Def5;ex e being object st

( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

let v, w, e0 be object ; :: thesis: ( e0 Joins v,w,G2 implies ex e being object st

( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) ) )

A6: ( v is set & w is set ) by TARSKI:1;

assume A7: e0 Joins v,w,G2 ; :: thesis: ex e being object st

( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

then A8: e0 Joins v,w,G1 by A6, GLIB_000:72;

then consider e being object such that

A9: ( e Joins v,w,G1 & e in E ) and

A10: for e9 being object st e9 Joins v,w,G1 & e9 in E holds

e9 = e by Def5;

take e = e; :: thesis: ( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

A11: not e in G1 .loops()

hence e Joins v,w,G2 by A6, A9, GLIB_000:73; :: thesis: ( e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

thus e in E \ (G1 .loops()) by A9, A11, XBOOLE_0:def 5; :: thesis: for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) implies e9 = e )

assume ( e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) ) ; :: thesis: e9 = e

then ( e9 Joins v,w,G1 & e9 in E \ (G1 .loops()) ) by A6, GLIB_000:72;

then ( e9 Joins v,w,G1 & e9 in E ) by XBOOLE_1:36, TARSKI:def 3;

hence e9 = e by A10; :: thesis: verum

end;( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) ) )

A6: ( v is set & w is set ) by TARSKI:1;

assume A7: e0 Joins v,w,G2 ; :: thesis: ex e being object st

( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

then A8: e0 Joins v,w,G1 by A6, GLIB_000:72;

then consider e being object such that

A9: ( e Joins v,w,G1 & e in E ) and

A10: for e9 being object st e9 Joins v,w,G1 & e9 in E holds

e9 = e by Def5;

take e = e; :: thesis: ( e Joins v,w,G2 & e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

A11: not e in G1 .loops()

proof

e in the_Edges_of G2
by A4, A9, A11, XBOOLE_0:def 5;
assume
e in G1 .loops()
; :: thesis: contradiction

then consider u being object such that

A12: e Joins u,u,G1 by Def2;

( v = u & w = u ) by A9, A12, GLIB_000:15;

then A13: e0 in G1 .loops() by A8, Def2;

e0 in the_Edges_of G2 by A7, GLIB_000:def 13;

hence contradiction by A4, A13, XBOOLE_0:def 5; :: thesis: verum

end;then consider u being object such that

A12: e Joins u,u,G1 by Def2;

( v = u & w = u ) by A9, A12, GLIB_000:15;

then A13: e0 in G1 .loops() by A8, Def2;

e0 in the_Edges_of G2 by A7, GLIB_000:def 13;

hence contradiction by A4, A13, XBOOLE_0:def 5; :: thesis: verum

hence e Joins v,w,G2 by A6, A9, GLIB_000:73; :: thesis: ( e in E \ (G1 .loops()) & ( for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e ) )

thus e in E \ (G1 .loops()) by A9, A11, XBOOLE_0:def 5; :: thesis: for e9 being object st e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) implies e9 = e )

assume ( e9 Joins v,w,G2 & e9 in E \ (G1 .loops()) ) ; :: thesis: e9 = e

then ( e9 Joins v,w,G1 & e9 in E \ (G1 .loops()) ) by A6, GLIB_000:72;

then ( e9 Joins v,w,G1 & e9 in E ) by XBOOLE_1:36, TARSKI:def 3;

hence e9 = e by A10; :: thesis: verum

A14: the_Vertices_of G3 = the_Vertices_of G2 by A3, A4;

E \ (G1 .loops()) c= (the_Edges_of G1) \ (G1 .loops()) by XBOOLE_1:33;

then A15: G3 is Subgraph of G2 by A1, A2, 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;

then G3 is inducedSubgraph of G2, the_Vertices_of G2,E2 by A3, A14, A15, GLIB_000:def 37;

hence G3 is removeParallelEdges of G2 by Def7; :: thesis: verum