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