theorem Th9: :: NOMIN_2:9

for V, A being set
for d1, d2 being NonatomicND of V,A holds global_overlapping (V,A,d1,d2) is NonatomicND of V,A