:: deftheorem defines PPprediction PARTPR_2:def 6 :
for D being set holds PPprediction D = PFcompos (D,D,BOOLEAN);