let V, A be set ; :: thesis: {} in ND (V,A)
{} is NonatomicND of V,A by Th30;
hence {} in ND (V,A) ; :: thesis: verum