for G being _Graph holds id (the_Vertices_of G) is directed continuous Dcontinuous PVertexMapping of G,G