{v,v1} c= V by ZFMISC_1:32;
hence ND_ex_2 (v,v1,a) is NonatomicND of V,A by Th49; :: thesis: verum