theorem Th25: :: PARTPR_1:25

for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_and (p,q)) & (PP_and (p,q)) . x = FALSE & not ( x in dom p & p . x = FALSE ) holds
( x in dom q & q . x = FALSE )