:: deftheorem Def13 defines naming NOMIN_1:def 13 :
for V, A being set
for v, D being object st D is TypeSCNominativeData of V,A & v in V holds
naming (V,A,v,D) = v .--> D;