theorem :: GLIB_013:17

for G being _Graph holds
( G is edge-finite iff ex n being Nat st G is n -edge )