let V, A be set ; :: thesis: 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; :: thesis: ( D1 tolerates D2 implies D1 +* D2 is NonatomicND of V,A )

assume A1: D1 tolerates D2 ; :: thesis: 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; :: thesis: verum

D1 +* D2 is NonatomicND of V,A

let D1, D2 be NonatomicND of V,A; :: thesis: ( D1 tolerates D2 implies D1 +* D2 is NonatomicND of V,A )

assume A1: D1 tolerates D2 ; :: thesis: 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; :: thesis: verum