theorem Th4: :: NOMIN_1:4

for x being object
for V, A being set st x in NDSS (V,A) holds
x is TypeSSNominativeData of V,A