for a, v being object
for V, A being set st v in V & a in A holds
ND_ex_1 (v,a) is TypeSCNominativeData of V,A by Th46;