theorem :: PARTPR_1:7

for x being object
for D being set
for p being PartialPredicate of D st x in dom (PP_not p) & (PP_not p) . x = TRUE holds
( x in dom p & p . x = FALSE )