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