let G1, G2 be _Graph; :: thesis: for G3 being removeParallelEdges of G1 st G2 == G3 holds
G2 is removeParallelEdges of G1
let G3 be removeParallelEdges of G1; :: thesis: ( G2 == G3 implies G2 is removeParallelEdges of G1 )
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;
assume G2 == G3 ; :: thesis: G2 is removeParallelEdges of G1
then G2 is inducedSubgraph of G1, the_Vertices_of G1,E by A1, GLIB_000:101;
hence G2 is removeParallelEdges of G1 by Def7; :: thesis: verum