dom F = dom (the_Vertices_of F) by Def4;
hence the_Vertices_of F is empty ; :: thesis: verum