theorem Th7: :: GLIB_013:7

for G being _Graph holds
( G is edge-finite iff G .size() is finite ) ;