theorem :: PARTPR_1:53

for D being non empty set
for p being PartialPredicate of D holds PP_imp ((PP_False D),p) = PP_True D