:: deftheorem defines Pr PARTPR_1:def 1 :
for D being set holds Pr D = PFuncs (D,BOOLEAN);