theorem Th8: :: NOMIN_4:8

for V, A being set
for a being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) holds
rng (denaming (V,A,a)) c= A