theorem Th6: :: NOMIN_3:6

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