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