theorem Th33: :: NOMIN_1:33

for V, A being set
for D being NonatomicND of V,A ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))