theorem :: NOMIN_3:2

for D being set
for p being PartialPredicate of D holds PPid D coincides_with p ;