let V, A be set ; :: thesis: for D being NonatomicND of V,A st not D in A holds
global_overlapping (V,A,D,D) = D
let D be NonatomicND of V,A; :: thesis: ( not D in A implies global_overlapping (V,A,D,D) = D )
dom D c= dom D ;
hence ( not D in A implies global_overlapping (V,A,D,D) = D ) by Th65; :: thesis: verum