theorem :: PARTPR_1:2

for D being set
for p being PartialPredicate of D holds p in Pr D by PARTFUN1:45;