theorem :: NOMIN_3:9

for D being non empty set
for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds
PP_or (p,r) ||= PP_or (q,s)