theorem :: PARTPR_1:21

for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & (PP_and (p,q)) . x = TRUE holds
p . x = TRUE by Th3, Th19;