let G be _Graph; :: thesis: ( G is vertex-finite iff ex n being non zero Nat st G is n -vertex )

hereby :: thesis: ( ex n being non zero Nat st G is n -vertex implies G is vertex-finite )

assume G is vertex-finite ; :: thesis: ex n being non zero Nat st G is n -vertex
then reconsider n = card (the_Vertices_of G) as Nat ;
reconsider n = n as non zero Nat ;
take n = n; :: thesis: G is n -vertex
thus G is n -vertex ; :: thesis: verum

end;

thus ( ex n being non zero Nat st G is n -vertex implies G is vertex-finite ) ; :: thesis: verum