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