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