take the NonatomicND of V,A ; :: thesis: ( the NonatomicND of V,A in A or the NonatomicND of V,A is NonatomicND of V,A )
thus ( the NonatomicND of V,A in A or the NonatomicND of V,A is NonatomicND of V,A ) ; :: thesis: verum