:: deftheorem defines PP_id PARTPR_2:def 3 :
for D being non empty set
for d being Element of D holds PP_id d = (PPid D) . d;