let V, A be set ; :: thesis: for D being NonatomicND of V,A holds global_overlapping (V,A,D,D) = D
let D be NonatomicND of V,A; :: thesis: global_overlapping (V,A,D,D) = D

per cases ( not D in A or D in A ) ;

suppose A1: not D in A ; :: thesis: global_overlapping (V,A,D,D) = D

dom D c= dom D ;
hence global_overlapping (V,A,D,D) = D by A1, Th65; :: thesis: verum

end;

suppose A2: D in A ; :: thesis: global_overlapping (V,A,D,D) = D

D is TypeSCNominativeData of V,A by Def6;
hence global_overlapping (V,A,D,D) = D by A2, Def16; :: thesis: verum

end;

end;