theorem Th3: :: NOMIN_5:3

for v, v1 being object
for V, A being set
for d1 being NonatomicND of V,A
for T being TypeSCNominativeData of V,A st A is_without_nonatomicND_wrt V & v in V & v <> v1 & v1 in dom d1 holds
(local_overlapping (V,A,d1,T,v)) . v1 = d1 . v1