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