theorem :: NOMIN_1:50

for a1, v, v1 being object
for V, A being set st {v,v1} c= V & a1 in A holds
ND_ex_2 (v,v1,a1) is TypeSCNominativeData of V,A by Th49;