theorem :: NOMIN_3:17

for D being non empty set
for p being PartialPredicate of D holds <*p,(PPid D),p*> is SFHT of D