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