:: deftheorem Def13 defines PartialPredConnectivesCompl PARTPR_1:def 13 :
for D being non empty set
for b₂ being UnOp of (Pr D) holds
( b₂ = PartialPredConnectivesCompl D iff for p being PartialPredicate of D holds b₂ . p = PP_not p );