:: deftheorem defines PPcomposition PARTPR_2:def 4 :
for D being set holds PPcomposition D = PFcompos (D,D,D);