:: deftheorem defines local_overlapping NOMIN_1:def 17 :
for V, A being set
for d1, d2, v being object holds local_overlapping (V,A,d1,d2,v) = global_overlapping (V,A,d1,(naming (V,A,v,d2)));