theorem Th8: :: PARTPR_1:8

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