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