theorem Th18: :: NOMIN_2:19

for v, x being object
for V, A being set
for p being SCPartialNominativePredicate of V,A holds
( not x in dom (SC_exists (p,v)) or ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) )