A1: {v,v1,v2} c= V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v,v1,v2} or x in V )
assume x in {v,v1,v2} ; :: thesis: x in V
then ( x = v or x = v1 or x = v2 ) by ENUMSET1:def 1;
hence x in V ; :: thesis: verum

end;

{a,a1} c= A by ZFMISC_1:32;
hence ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A by A1, Th55; :: thesis: verum