:: deftheorem defines is_ext_real_on NOMIN_4:def 4 :
for V, A being set
for d being TypeSCNominativeData of V,A
for a being Element of V holds
( a is_ext_real_on d iff (denaming (V,A,a)) . d is ext-real );