theorem :: PARTPR_1:59

for D being non empty set holds PP_imp ((PP_BottomPred D),(PP_True D)) = PP_True D