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