:: deftheorem defines is_a_value_on NOMIN_4:def 6 :
for V, A being set
for d being TypeSCNominativeData of V,A
for a being Element of V holds
( a is_a_value_on d iff (denaming (V,A,a)) . d in A );