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