theorem :: NOMIN_3:10

for D being non empty set
for p, q, r being PartialPredicate of D st PP_or (p,q) ||= r holds
PP_and (p,q) ||= r by Th6, Th3;