let V, A be set ; :: thesis: for D being NonatomicND of V,A holds D in ND (V,A)
let D be NonatomicND of V,A; :: thesis: D in ND (V,A)
D is TypeSCNominativeData of V,A by Def6;
hence D in ND (V,A) ; :: thesis: verum