let V, A be set ; for d1, d2 being NonatomicND of V,A holds global_overlapping (V,A,d1,d2) is NonatomicND of V,A
let d1, d2 be NonatomicND of V,A; global_overlapping (V,A,d1,d2) is NonatomicND of V,A
per cases
( ( not d1 in A & not d2 in A ) or d1 in A or d2 in A )
;
suppose
( not
d1 in A & not
d2 in A )
;
global_overlapping (V,A,d1,d2) is NonatomicND of V,Athen A1:
global_overlapping (
V,
A,
d1,
d2)
= d2 \/ (d1 | ((dom d1) \ (dom d2)))
by NOMIN_1:64;
d1 | ((dom d1) \ (dom d2)) is
NonatomicND of
V,
A
by NOMIN_1:32, RELAT_1:59;
hence
global_overlapping (
V,
A,
d1,
d2) is
NonatomicND of
V,
A
by A1, NOMIN_1:36, PARTFUN1:51;
verum end; end;