:: deftheorem defines PP_and PARTPR_1:def 6 :
for D being non empty set
for p, q being PartialPredicate of D holds PP_and (p,q) = PP_not (PP_or ((PP_not p),(PP_not q)));