theorem Th49: :: PARTPR_1:49

for D being non empty set
for p being PartialPredicate of D holds PP_or (p,(PP_not p)) = (PP_True D) | (dom p)