:: deftheorem defines NDSS NOMIN_1:def 2 :
for V, A being set holds NDSS (V,A) = { d where d is TypeSSNominativeData of V,A : verum } ;