card S is finite ;
then card (the_Edges_of S) is finite by Th7, FINSET_1:1;
hence the_Edges_of S is finite ; :: thesis: verum