:: deftheorem defines ND NOMIN_1:def 7 :
for V, A being set holds ND (V,A) = { D where D is TypeSCNominativeData of V,A : verum } ;