let V, A be set ; :: thesis: for d being object st d in nonatomicsND (V,A) holds
d is NonatomicND of V,A
let d be object ; :: thesis: ( d in nonatomicsND (V,A) implies d is NonatomicND of V,A )
assume d in nonatomicsND (V,A) ; :: thesis: d is NonatomicND of V,A
then ex d1 being NonatomicND of V,A st d = d1 ;
hence d is NonatomicND of V,A ; :: thesis: verum