theorem Th55: :: NOMIN_1:55

for a, a1, v, v1, v2 being object
for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds
ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A