theorem :: PARTPR_1:52

for D being non empty set
for p being PartialPredicate of D holds PP_and ((PP_not p),p) = (PP_False D) | (dom p) by Th51;