let V, A be set ; for D1, D2 being NonatomicND of V,A st D1 tolerates D2 holds
D1 +* D2 is NonatomicND of V,A
let D1, D2 be NonatomicND of V,A; ( D1 tolerates D2 implies D1 +* D2 is NonatomicND of V,A )
assume A1:
D1 tolerates D2
; D1 +* D2 is NonatomicND of V,A
then
D1 \/ D2 = D1 +* D2
by FUNCT_4:30;
hence
D1 +* D2 is NonatomicND of V,A
by A1, Th36; verum