theorem :: NOMIN_1:53

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