theorem :: NOMIN_3:27

for D being non empty set
for f being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D holds
<*(PP_or (p,q)),f,r*> is SFHT of D