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