theorem Th4: :: NOMIN_4:4

for v being object
for V, A being set st A is_without_nonatomicND_wrt V & v in V holds
for d1 being NonatomicND of V,A
for d2 being TypeSCNominativeData of V,A holds dom (local_overlapping (V,A,d1,d2,v)) = {v} \/ (dom d1)