let V, A be set ; :: thesis: for D1, D2 being NonatomicND of V,A st not D1 in A & not D2 in A & dom D1 c= dom D2 holds
global_overlapping (V,A,D1,D2) = D2
let D1, D2 be NonatomicND of V,A; :: thesis: ( not D1 in A & not D2 in A & dom D1 c= dom D2 implies global_overlapping (V,A,D1,D2) = D2 )
assume A1: ( not D1 in A & not D2 in A ) ; :: thesis: ( not dom D1 c= dom D2 or global_overlapping (V,A,D1,D2) = D2 )
assume A2: dom D1 c= dom D2 ; :: thesis: global_overlapping (V,A,D1,D2) = D2
thus global_overlapping (V,A,D1,D2) = D2 \/ (D1 | ((dom D1) \ (dom D2))) by A1, Th64
.= D2 \/ (D1 | {}) by A2, XBOOLE_1:37
.= D2 ; :: thesis: verum