:: deftheorem Def6 defines TypeSCNominativeData NOMIN_1:def 6 :
for V, A, b₃ being set holds
( b₃ is TypeSCNominativeData of V,A iff ( b₃ in A or b₃ is NonatomicND of V,A ) );