reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
D . n1 is non empty set ;
hence not D . n is empty ; :: thesis: verum