the carrier' of G is finite by GRAPH_1:def 11;
hence Edges_In (v,X) is finite ; :: thesis: verum