theorem Th5: :: GLIB_011:5

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