:: deftheorem defines SC_name_check NOMIN_2:def 17 :
for V, A being set
for v being object
for b₄ being SCPartialNominativePredicate of V,A holds
( b₄ = SC_name_check (V,A,v) iff ( dom b₄ = (ND (V,A)) \ A & ( for d being NonatomicND of V,A st d in dom b₄ holds
( ( denaming (v,d) in dom b₄ implies b₄ . d = TRUE ) & ( not denaming (v,d) in dom b₄ implies b₄ . d = FALSE ) ) ) ) );