theorem Th9: :: PARTPR_1:9

for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & x in dom q & (PP_or (p,q)) . x = TRUE & not p . x = TRUE holds
q . x = TRUE