let G1, G2 be _Graph; :: thesis: for G3 being DSimpleGraph of G1 st G1 == G2 holds

G3 is DSimpleGraph of G2

let G3 be DSimpleGraph of G1; :: thesis: ( G1 == G2 implies G3 is DSimpleGraph of G2 )

consider E being RepDEdgeSelection of G1 such that

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

assume A2: G1 == G2 ; :: thesis: G3 is DSimpleGraph of G2

then A3: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by GLIB_000:def 34;

then A4: G3 is inducedSubgraph of G2, the_Vertices_of G2,E \ (G1 .loops()) by A1, A2, GLIB_000:95;

A5: G1 .loops() = G2 .loops() by A2, Th50;

G2 is Subgraph of G1 by A2, GLIB_000:87;

then E is RepDEdgeSelection of G2 by A3, Th79;

hence G3 is DSimpleGraph of G2 by A4, A5, Def10; :: thesis: verum

G3 is DSimpleGraph of G2

let G3 be DSimpleGraph of G1; :: thesis: ( G1 == G2 implies G3 is DSimpleGraph of G2 )

consider E being RepDEdgeSelection of G1 such that

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

assume A2: G1 == G2 ; :: thesis: G3 is DSimpleGraph of G2

then A3: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by GLIB_000:def 34;

then A4: G3 is inducedSubgraph of G2, the_Vertices_of G2,E \ (G1 .loops()) by A1, A2, GLIB_000:95;

A5: G1 .loops() = G2 .loops() by A2, Th50;

G2 is Subgraph of G1 by A2, GLIB_000:87;

then E is RepDEdgeSelection of G2 by A3, Th79;

hence G3 is DSimpleGraph of G2 by A4, A5, Def10; :: thesis: verum