let V, A be 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)))
let D1, D2 be NonatomicND of V,A; ( not D1 in A & not D2 in A implies global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2))) )
A1:
D1 is TypeSCNominativeData of V,A
by Def6;
A2:
D2 is TypeSCNominativeData of V,A
by Def6;
assume
( not D1 in A & not D2 in A )
; global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))
then
ex f1, f2 being Function st
( f1 = D1 & f2 = D2 & global_overlapping (V,A,D1,D2) = f2 \/ (f1 | ((dom f1) \ (dom f2))) )
by A1, A2, Def16;
hence
global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2)))
; verum