:: deftheorem defines PP_or PARTPR_1:def 5 :
for D being non empty set
for p, q being PartialPredicate of D holds PP_or (p,q) = (PPdisjunction D) . (p,q);