:: deftheorem Def1 defines vertex-finite GLIB_013:def 1 :
for G being _Graph holds
( G is vertex-finite iff the_Vertices_of G is finite );