let G2 be Subgraph of G; :: thesis: G2 is edge-finite
the_Edges_of G2 c= the_Edges_of G ;
hence G2 is edge-finite ; :: thesis: verum