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

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 )
;

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;hence global_overlapping (V,A,D,D) = D by A2, Def16; :: thesis: verum