theorem :: PARTPR_1:48

for D being non empty set
for p being PartialPredicate of D holds PP_and ((PP_False D),p) = PP_False D by Th47;