:: deftheorem Def2 defines PPnegation PARTPR_1:def 2 :
for D being set
for b₂ being Function of (Pr D),(Pr D) holds
( b₂ = PPnegation D iff for p being PartialPredicate of D holds
( dom (b₂ . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b₂ . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b₂ . p) . d = TRUE ) ) ) ) );