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

hereby :: thesis: ( ex n being Nat st G is n -edge implies G is edge-finite )

assume G is edge-finite ; :: thesis: ex n being Nat st G is n -edge
then reconsider n = card (the_Edges_of G) as Nat ;
take n = n; :: thesis: G is n -edge
thus G is n -edge ; :: thesis: verum

end;

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