for V, A being set
for i, j, b, n, s being Element of V
for i1, j1, b1, n1, s1 being object
for d1, Li, Lj, Lb, Ln, Ls being NonatomicND of V,A
for Di, Dj, Db, Dn, Ds being SCBinominativeFunction of V,A st not V is empty & A is_without_nonatomicND_wrt V & Di = denaming (V,A,i1) & Dj = denaming (V,A,j1) & Db = denaming (V,A,b1) & Dn = denaming (V,A,n1) & Ds = denaming (V,A,s1) & Li = local_overlapping (V,A,d1,(Di . d1),i) & Lj = local_overlapping (V,A,Li,(Dj . Li),j) & Lb = local_overlapping (V,A,Lj,(Db . Lj),b) & Ln = local_overlapping (V,A,Lb,(Dn . Lb),n) & Ls = local_overlapping (V,A,Ln,(Ds . Ln),s) & j1 in dom d1 & b1 in dom d1 & n1 in dom d1 & s1 in dom d1 & d1 in dom Di & s <> n holds
Ls . n = Ln . n