Description: The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 13-Oct-2020)