let V, A be set ; :: thesis: ( A is_without_nonatomicND_wrt V implies for d being NonatomicND of V,A holds not d in A )
assume A1: A is_without_nonatomicND_wrt V ; :: thesis: for d being NonatomicND of V,A holds not d in A
let d be NonatomicND of V,A; :: thesis: not d in A
d in nonatomicsND (V,A) ;
hence not d in A by A1, XBOOLE_0:3; :: thesis: verum