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