let G be _Graph; :: thesis: ( G is edge-finite & G is connected implies ( G is vertex-finite & G is _finite ) )
assume A1: ( G is edge-finite & G is connected ) ; :: thesis: ( G is vertex-finite & G is _finite )
thus G is vertex-finite :: thesis: G is _finite

proof

assume not G is vertex-finite ; :: thesis: contradiction
then reconsider G9 = G as non vertex-finite edge-finite _Graph by A1;
set v = the isolated Vertex of G9;
{ the isolated Vertex of G9} = G9 .reachableFrom the isolated Vertex of G9 by GLIB_006:51
.= the_Vertices_of G9 by A1, GLIB_002:16 ;
hence contradiction ; :: thesis: verum

end;

hence G is _finite by A1; :: thesis: verum