theorem Th17: :: GLUNIR00:17

for G being _Graph
for H being removeLoops of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))