theorem Th9: :: NOMIN_4:9

for V, A being set
for a, b being Element of V st ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) holds
rng <:(denaming (V,A,a)),(denaming (V,A,b)):> c= [:A,A:]