theorem :: GLIB_013:16

for G being _Graph holds
( G is vertex-finite iff ex n being non zero Nat st G is n -vertex )