:: deftheorem defines PPBottomFunc PARTPR_2:def 10 :
for D being set holds PPBottomFunc D = {} ;