L `1 in bool (the_Vertices_of G) by MCART_1:10;
hence L `1 is finite ; :: thesis: verum