theorem Th6: :: GLIB_013:6

for G being _Graph holds
( G is vertex-finite iff G .order() is finite ) ;