( {v,v1} c= V & {a,a1} c= A ) by ZFMISC_1:32;
hence ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A by Th52; :: thesis: verum