let G1 be non-Dmulti _Graph; :: thesis: for G2 being _Graph holds

( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )

let G2 be _Graph; :: thesis: ( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )

set E = the RepDEdgeSelection of G1;

the RepDEdgeSelection of G1 = the_Edges_of G1 by Th76;

hence G2 is DSimpleGraph of G1 by A2, Def10; :: thesis: verum

( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )

let G2 be _Graph; :: thesis: ( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )

hereby :: thesis: ( G2 is removeLoops of G1 implies G2 is DSimpleGraph of G1 )

assume A2:
G2 is removeLoops of G1
; :: thesis: G2 is DSimpleGraph of G1assume
G2 is DSimpleGraph of G1
; :: thesis: G2 is removeLoops of G1

then consider E being RepDEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops()) by Def10;

thus G2 is removeLoops of G1 by A1, Th76; :: thesis: verum

end;then consider E being RepDEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops()) by Def10;

thus G2 is removeLoops of G1 by A1, Th76; :: thesis: verum

set E = the RepDEdgeSelection of G1;

the RepDEdgeSelection of G1 = the_Edges_of G1 by Th76;

hence G2 is DSimpleGraph of G1 by A2, Def10; :: thesis: verum