Description: The set of vertices of a graph. (Contributed by AV, 9-Jan-2020) (Revised by AV, 21-Sep-2020)