let G1, G2 be _Graph; :: thesis: for G3 being removeParallelEdges of G1 st G1 == G2 holds
G3 is removeParallelEdges of G2
let G3 be removeParallelEdges of G1; :: thesis: ( G1 == G2 implies G3 is removeParallelEdges of G2 )
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;
assume A2: G1 == G2 ; :: thesis: G3 is removeParallelEdges 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 by A1, A2, GLIB_000:95;
G2 is Subgraph of G1 by A2, GLIB_000:87;
then E is RepEdgeSelection of G2 by A3, Th78;
hence G3 is removeParallelEdges of G2 by A4, Def7; :: thesis: verum