:: deftheorem defines PP_not PARTPR_1:def 3 :
for D being set
for p being PartialPredicate of D holds PP_not p = (PPnegation D) . p;