theorem Th12: :: NOMIN_2:13

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