theorem Th34: :: PARTPR_1:34

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