:: deftheorem defines PP_BottomPred PARTPR_1:def 10 :
for D being set holds PP_BottomPred D = {} ;