let G be _Graph; :: thesis: for H being DSimpleGraph of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
let H be DSimpleGraph of G; :: thesis: VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
consider G9 being removeDParallelEdges of G such that
A1: H is removeLoops of G9 by GLIB_009:120;
A2: the_Vertices_of G9 = the_Vertices_of G by GLIB_000:def 33;
thus VertexDomRel H = (VertexDomRel G9) \ (id (the_Vertices_of G9)) by A1, Th17
.= (VertexDomRel G) \ (id (the_Vertices_of G)) by A2, Th16 ; :: thesis: verum