theorem Th3: :: NOMIN_3:3

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