for G being _Graph holds
( G is vertex-finite iff ex n being non zero Nat st G is n -vertex )