Description: The class of neighbors of a vertex in a finite simple graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018) (Revised by AV, 28-Oct-2020)