theorem Th5: :: PARTPR_1:5

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