:: deftheorem Def2 defines edge-finite GLIB_013:def 2 :
for G being _Graph holds
( G is edge-finite iff the_Edges_of G is finite );