:: deftheorem Def17 defines _finite GLIB_000:def 17 :
for G being _Graph holds
( G is _finite iff ( the_Vertices_of G is finite & the_Edges_of G is finite ) );