theorem Th12: :: NOMIN_4:12

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
dom (less (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))