theorem :: GLIB_015:25

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