theorem :: PARTPR_1:38

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