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

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