let G be Singlification of A,k; :: thesis: not G is empty
dom G = dom A by Def6;
hence not G is empty ; :: thesis: verum