theorem Th6: :: NOMIN_4:6

for v being object
for V, A being set
for d being TypeSCNominativeData of V,A
for d1 being NonatomicND of V,A st v in V & A is_without_nonatomicND_wrt V holds
local_overlapping (V,A,d1,d,v) in dom (denaming (V,A,v))