let G be _Graph; :: thesis: for H being removeDParallelEdges of G holds VertexDomRel H = VertexDomRel G
let H be removeDParallelEdges of G; :: thesis: VertexDomRel H = VertexDomRel G
consider E being RepDEdgeSelection of G such that
A1: H is inducedSubgraph of G, the_Vertices_of G,E by GLIB_009:def 8;
A2: VertexDomRel H c= VertexDomRel G by Th15;

now :: thesis: for v, w being object st [v,w] in VertexDomRel G holds
[v,w] in VertexDomRel H

let v, w be object ; :: thesis: ( [v,w] in VertexDomRel G implies [v,w] in VertexDomRel H )
assume [v,w] in VertexDomRel G ; :: thesis: [v,w] in VertexDomRel H
then consider e0 being object such that
A3: e0 DJoins v,w,G by Th1;
( the_Edges_of G = G .edgesBetween (the_Vertices_of G) & the_Vertices_of G c= the_Vertices_of G ) by GLIB_000:34;
then A4: the_Edges_of H = E by A1, GLIB_000:def 37;
consider e being object such that
A5: ( e DJoins v,w,G & e in E ) and
for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = e by A3, GLIB_009:def 6;
( v is set & w is set ) by TARSKI:1;
then e DJoins v,w,H by A4, A5, GLIB_000:73;
hence [v,w] in VertexDomRel H by Th1; :: thesis: verum

end;

then VertexDomRel G c= VertexDomRel H by RELAT_1:def 3;
hence VertexDomRel H = VertexDomRel G by A2, XBOOLE_0:def 10; :: thesis: verum