theorem Th64: :: NOMIN_1:64

for V, A being set
for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A holds
global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))