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