theorem :: GLUNIR00:18
for G being _Graph
for H being DSimpleGraph of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))