dom F = dom (the_Edges_of F) by Def5;
hence not the_Edges_of F is empty ; :: thesis: verum