A1: dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;
then rng (the_VLabel_of G) is finite by FINSET_1:8;
hence the_VLabel_of G is finite by A1, ORDERS_1:87; :: thesis: verum