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