let V, A be set ; :: thesis: 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; :: thesis: 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 ) ; :: thesis: global_overlapping (V,A,d1,d2) is NonatomicND of V,A
then 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; :: thesis: verum
end;
suppose ( d1 in A or d2 in A ) ; :: thesis: global_overlapping (V,A,d1,d2) is NonatomicND of V,A
hence global_overlapping (V,A,d1,d2) is NonatomicND of V,A by NOMIN_1:def 16; :: thesis: verum
end;
end;