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