dom (L `1) c= the_Vertices_of G ;
hence L `1 is finite by FINSET_1:29; :: thesis: verum