dom (IncAddr F,k) = dom F by Def15;
hence not IncAddr F,k is empty ; :: thesis: verum