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

hence ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A by A1, Th55; :: thesis: verum

proof

{a,a1} c= A
by ZFMISC_1:32;
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;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

hence ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A by A1, Th55; :: thesis: verum