dom (L `1) c= the_Vertices_of G ;
hence for b<sub>1</sub> being set st b<sub>1</sub> = L `1 holds
b₁ is finite by FINSET_1:10; :: thesis: verum