theorem Th29: :: PARTPR_1:29

for D being non empty set
for p, q being PartialPredicate of D holds PP_and (p,(PP_or (p,q))) = p