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

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