theorem Th6: :: NOMIN_2:6

for V, A being set
for D being finite Function st dom D c= V & rng D c= ND (V,A) holds
D is NonatomicND of V,A