theorem Th56: :: PARTPR_1:56

for D being set holds PP_not (PP_BottomPred D) = PP_BottomPred D