theorem :: GLIB_015:24

for F being Graph-yielding Function holds the_Vertices_of (rng F) = rng (the_Vertices_of F)