let G be _Graph; for H being removeDParallelEdges of G holds VertexDomRel H = VertexDomRel G
let H be removeDParallelEdges of G; 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 for v, w being object st [v,w] in VertexDomRel G holds
[v,w] in VertexDomRel Hlet v,
w be
object ;
( [v,w] in VertexDomRel G implies [v,w] in VertexDomRel H )assume
[v,w] in VertexDomRel G
;
[v,w] in VertexDomRel Hthen 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;
verum end;
then
VertexDomRel G c= VertexDomRel H
by RELAT_1:def 3;
hence
VertexDomRel H = VertexDomRel G
by A2, XBOOLE_0:def 10; verum