dom (the_ELabel_of G) c= the_Edges_of G by Lm1;
then A1: dom (the_ELabel_of G) is finite ;
then rng (the_ELabel_of G) is finite by FINSET_1:26;
hence the_ELabel_of G is finite by A1, ORDERS_1:197; :: thesis: verum