theorem :: PARTPR_1:37

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