:: deftheorem defines PP_inversion PARTPR_2:def 18 :
for D being non empty set
for p being PartialPredicate of D holds PP_inversion p = (PPinversion D) . p;