:: deftheorem Def19 defines PPinversion PARTPR_2:def 17 :
for D being non empty set
for b₂ being Function of (Pr D),(Pr D) holds
( b₂ = PPinversion D iff for p being PartialPredicate of D holds
( dom (b₂ . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds
(b₂ . p) . d = TRUE ) ) );